From 95740167c0f696764ccf1973e75888a88f56841f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 04:23:00 +0000 Subject: [PATCH 1/2] 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 a07b5cce286968319b55611b8ec8d911d3633289 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 07:33:10 +0000 Subject: [PATCH 2/2] 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.