From 95740167c0f696764ccf1973e75888a88f56841f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 04:23:00 +0000 Subject: [PATCH 1/4] Fix build against Rocq dev (9.4+alpha): qualify Constr.in_context 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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- LibHyps/LibHypsNaming.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LibHyps/LibHypsNaming.v b/LibHyps/LibHypsNaming.v index 9ba2f9e..983fef8 100644 --- a/LibHyps/LibHypsNaming.v +++ b/LibHyps/LibHypsNaming.v @@ -373,7 +373,7 @@ Module Ltac2. let nme_c:constr := Unsafe.make (Var(nme)) in let subth' := Constr.Unsafe.substnl [nme_c] 0 subth in rename_hyp_chained_quantifs stop acc subth' in - let _ := in_context nme typ tac_under_binder in + let _ := Constr.in_context nme typ tac_under_binder in () else rename_hyp_chained_quantifs stop acc subth @@ -399,7 +399,7 @@ Module Ltac2. let nme_c:constr := Unsafe.make (Var(nme)) in let subth' := Constr.Unsafe.substnl [nme_c] 0 subth in rename_hyp_chained_quantifs newstop acc subth' in - let _ := in_context nme typ tac_under_binder in + let _ := Constr.in_context nme typ tac_under_binder in () else @@ -461,7 +461,7 @@ Module Ltac2. kept *) Ltac2 in_context_then_forget nme typ f := Control.once_plus - (fun () => let _ := in_context nme typ f in backtrack "forget in_context subgoal") + (fun () => let _ := Constr.in_context nme typ f in backtrack "forget in_context subgoal") (fun _ => ()). Ltac2 rename_acc n th := From 0b5851b5dddb8b561a2d951a37455380d9c29bfa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 05:51:51 +0000 Subject: [PATCH 2/4] Fix LibHyps logical library mapping --- resources/coq_project.libhyps | 3 +-- resources/coq_project.tests | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/resources/coq_project.libhyps b/resources/coq_project.libhyps index 997cfc0..9136945 100644 --- a/resources/coq_project.libhyps +++ b/resources/coq_project.libhyps @@ -1,4 +1,3 @@ --R . LibHyps.LibHyps +-R . LibHyps -arg -w -arg -deprecated-since-9.0 - diff --git a/resources/coq_project.tests b/resources/coq_project.tests index 4b66821..83372ea 100644 --- a/resources/coq_project.tests +++ b/resources/coq_project.tests @@ -1,9 +1,8 @@ -R . LibHyps.tests --R ../LibHyps LibHyps.LibHyps +-R ../LibHyps LibHyps -arg -async-proofs-cache -arg force -arg -w -arg -undo-batch-mode -arg -w -arg -deprecated-since-9.0 - From a07b5cce286968319b55611b8ec8d911d3633289 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 07:33:10 +0000 Subject: [PATCH 3/4] Fix Not_focussed when LibHyps tactics run under a goal selector 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 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- LibHyps/TacNewHyps.v | 39 +++++++++++++++++++++++++++++---------- 1 file changed, 29 insertions(+), 10 deletions(-) diff --git a/LibHyps/TacNewHyps.v b/LibHyps/TacNewHyps.v index 90567b9..dad2901 100644 --- a/LibHyps/TacNewHyps.v +++ b/LibHyps/TacNewHyps.v @@ -61,22 +61,41 @@ Module Ltac2. Ltac2 iter_hyps (tac:ident -> unit) (lh:ident list) := List.iter tac lh. + (* [all_hyps_ident] calls [Control.hyps], which is a single-goal primitive: it raises + [Init.Not_focussed] whenever more than one goal is under focus. Every entry point that + reaches it must therefore run under [Control.enter]. + + This matters because these tactics are reached from Ltac1 through an [ltac2:()] quotation. + A plain Ltac1 tactic under a range selector is dispatched goal-wise by Ltac1 itself, so in + 4.0 -- where these were pure Ltac1 -- [1-4: onAllHyps ...] and [all: onAllHyps ...] simply + worked. The quotation evaluates in the multi-goal context instead, so the same script + raises [Not_focussed] and the goal-wise dispatch has to be reinstated explicitly. + Entering restores the 4.0 semantics rather than choosing new ones. *) Ltac2 map_all_hyps (tac:'a -> unit) := - let all_hyps := all_hyps_ident() in - iter_hyps tac all_hyps. + Control.enter + (fun () => + let all_hyps := all_hyps_ident() in + iter_hyps tac all_hyps). Ltac2 map_all_hyps_rev (tac: 'a -> unit) := - let all_hyps := List.rev (all_hyps_ident()) in - iter_hyps tac all_hyps. + Control.enter + (fun () => + let all_hyps := List.rev (all_hyps_ident()) in + iter_hyps tac all_hyps). + (* The inner [Control.enter] below guarded [hyps_after] only; [hyps_before] was computed in + whatever context the caller supplied and hit the same exception one line earlier. Entering + around the whole body also keeps [tac1] goal-wise, which is what Ltac1 did in 4.0. *) Ltac2 then_eachnh_gen (tac1:'a -> unit) (tac2:ident -> unit) (rev:bool) := - let hyps_before := all_hyps_ident() in - let _ := tac1() in Control.enter - (fun () => - let hyps_after := all_hyps_ident() in - let new_hyps: ident list := List.filter_out (fun id => List.mem Ident.equal id hyps_before) hyps_after in - iter_hyps tac2 (if rev then List.rev new_hyps else new_hyps)). + (fun () => + let hyps_before := all_hyps_ident() in + let _ := tac1() in + Control.enter + (fun () => + let hyps_after := all_hyps_ident() in + let new_hyps: ident list := List.filter_out (fun id => List.mem Ident.equal id hyps_before) hyps_after in + iter_hyps tac2 (if rev then List.rev new_hyps else new_hyps))). Ltac2 then_eachnh (tac1:'a -> unit) (tac2:ident -> unit) := then_eachnh_gen tac1 tac2 false. From fc5a0cf319b7b63565398860042cbb84220fb94f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 10 Aug 2026 17:25:57 +0000 Subject: [PATCH 4/4] Add coq-libhyps.opam as a wrapper, and conflict on the mismatched twin The repo ships only rocq-libhyps.opam, so `opam pin add coq-libhyps ` finds nothing repo-local and silently falls back to the package's *repository-cache* definition, keeping only the pin URL. On every switch here that fallback is the pre-split standalone recipe build: [ ["./configure.sh"] [make "-j%{jobs}%"] ] install: [make "install"] depends: [ "coq" {>= "8.11"} ] which builds the tree a second time and installs its own copy of the modules over the ones rocq-libhyps put there. After 0b5851b both packages target user-contrib/LibHyps/, so this is now a direct collision: opam lists both twins as installed while one of them has none of its recorded files on disk. It is not a loadpath problem -- `logpath:` in tags: is documentation for the archive website and does not affect where anything is written; the install prefix comes from `-R . LibHyps` in resources/coq_project.libhyps. Mirror the two archive rows so a pin of either name behaves the way the archive does: coq-libhyps.opam a pure wrapper -- no build:, no install:, one dependency `"rocq-libhyps" { = version }`. It installs nothing, so the collision cannot happen. rocq-libhyps.opam gains `conflicts: [ "coq-libhyps" { != version } ]`, which permits the matching wrapper and rejects any real coq-libhyps, i.e. exactly the pairs that would write the same paths. Both files are copies of extra-dev/packages/{coq,rocq}-libhyps/*.dev/opam at opam-coq-archive master (56ed7c2), consistent with the header comment both files already carry. Neither gets a `version:` field -- the archive rows supply the version, and hard-coding "dev" here would break the released tags. `opam lint` passes on both. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- coq-libhyps.opam | 21 +++++++++++++++++++++ rocq-libhyps.opam | 2 ++ 2 files changed, 23 insertions(+) create mode 100644 coq-libhyps.opam diff --git a/coq-libhyps.opam b/coq-libhyps.opam new file mode 100644 index 0000000..84e0a94 --- /dev/null +++ b/coq-libhyps.opam @@ -0,0 +1,21 @@ +# this is a mirror of an opam description file in the +# opam-coq-archive at: +# https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-libhyps +# the latter being official and probably more up to date. + +opam-version: "2.0" +maintainer: "Pierre.Courtieu@lecnam.net" + +homepage: "https://github.com/Matafou/LibHyps" +dev-repo: "git+https://github.com/Matafou/LibHyps.git" +bug-reports: "https://github.com/Matafou/LibHyps/issues" +doc: "https://github.com/Matafou/LibHyps/blob/master/Demo/demo.v" +license: "MIT" + +depends: [ "rocq-libhyps" { = version } ] + +authors: [ + "Pierre Courtieu" +] + +synopsis: "Compatibility package for rocq-libhyps" diff --git a/rocq-libhyps.opam b/rocq-libhyps.opam index 306a8f0..49dde9e 100644 --- a/rocq-libhyps.opam +++ b/rocq-libhyps.opam @@ -32,6 +32,8 @@ depends: [ "rocq-stdlib" ] +conflicts: [ "coq-libhyps" { != version } ] + tags: [ "keyword:proof environment manipulation" "keyword:forward reasoning"