Qualify Constr.in_context for Rocq dev

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 :=

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.