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 :=
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.
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/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
-
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"