Qualify Constr.in_context for Rocq dev - #19
Draft
JasonGross wants to merge 2 commits into
Draft
Conversation
Rocq dev added a new `Constr.Unsafe.in_context` primitive with an extra
`constr option` argument (the optional let-binding body), keeping the
old three-argument `Constr.in_context` as an Ltac2-level wrapper.
`LibHypsNaming.v` does `Import Constr.Unsafe.`, so the unqualified
`in_context` now resolves to the new four-argument `Unsafe` version:
Error: This expression has type unit -> unit
but an expression was expected of type constr option
Qualify the three call sites as `Constr.in_context`, which names the
same function on Coq 8.x / Rocq 9.0-9.3 as well.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Author
|
Superseded by #20, which retains the validated Claude compatibility commit and adds the required logical-library mapping fix on a distinct Codex branch. No changes were made to this PR's source branch. Authorship note: this was researched and written by an AI coding agent |
map_all_hyps, map_all_hyps_rev and then_eachnh_gen all reach
Control.hyps via all_hyps_ident. Control.hyps is a single-goal
primitive and raises Init.Not_focussed whenever more than one goal is
under focus, so any script writing
1-4: onAllHyps (fun h => idtac h)
all: onAllHypsRev (fun h => idtac h)
fails. In 4.0 these tactics were pure Ltac1 and a range selector
dispatched them goal-wise automatically; 5.0 routes them through an
ltac2:() quotation, which evaluates in the multi-goal context instead.
Wrap each entry point in Control.enter, which reinstates the goal-wise
dispatch rather than choosing new semantics. then_eachnh_gen already
had an inner Control.enter, but it guarded only hyps_after -- hyps_before
was computed in the caller's context and hit the exception one line
earlier.
Verified against rocq-dev 9.4+alpha:
- five repros covering onAllHyps / onAllHypsRev / then_eachnh under
`1-4:` and `all:` fail before and pass after; the single-focused-goal
case passed both before and after, which is why this went unnoticed
- tests/ is unchanged: all 14 files give byte-identical exit codes
before and after (3 pass, 9 pre-existing `no Ltac named rename_depth`,
2 pre-existing timeouts). The 3 that pass are the ones exercising
onAllHyps -- demo.v, LibHypsTest.v, LibHypsRegression.v
- coq-matching-logic, which broke at Syntax.v:2968 on `1-3: wf_auto2`,
now builds 87/87 with `dune build -p coq-matching-logic` (rc=0),
matching what it reaches against LibHyps 4.0.0
Found by port-frozen's 4.0-vs-5.0 A/B.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Rocq dev (9.4+alpha) resolves unqualified Ltac2
in_contextto this module'sunit -> unithelper instead of the constructor-context primitive. Qualify the three calls asConstr.in_context.Commit 9574016 was produced by a Claude coding agent. OpenAI Codex reproduced the failure and validated the library and tests:
opam exec --switch=rocq-dev-testing -- ./configure.shopam exec --switch=rocq-dev-testing -- make -j8 allAll library files and regression/demo tests pass.
Wordsmithed by Codex.