diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index b1fc8b75dc12a83fb115217103c82cf97935418b..6ca824570bf0c68d8b207a40a8e7cffa3f207e98 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -509,98 +509,117 @@ Tactic Notation "iter" tactic(tac) tactic(l) :=
 [generalize] and [specialize] with support for "o"pen terms. You can leave
 underscores that become evars or subgoals, similar to [refine]. *)
 
-(** The helper [opose_core p tac] introduces the uconstr [p] as a term into the
-context, making all underscores inside it evars and shelving all the ones that
-are unifiable (but leaving the non-unifiable ones unshelved). [tac] will be
-called with the name of that term in the context as argument (i.e., we have
-[i := p : type_of p]). That name is supposed to be temporary, and if [tac]
-does not rename/clear that name then it will be removed after [tac] is done.
-
-This may seem unnecessarily round-about, and indeed most users of [opose_core]
-could use a much simpler implementation, but some users need to inspect the term
-[p]. As a [uconstr] it cannot be inspected, and as an [open_constr] it will
-introduce a fresh set of shelved evars too early, before we can unshelve them.
-So we need to somehow convert [p] to a [constr], create the evars, shelve them,
-and do that all only once, and that's what this tactic does. *)
+(** The helper [opose_core p tac] takes a uconstr [p] and turns it into a constr
+that is passed to [tac]. All underscores inside [p] become evars, and the ones
+that are unifiable (i.e, appear in the type of other evars) are shelved.
+
+This is similar to creating a [open_constr], except that we have control over
+what does and does not get shelved. Creating a [open_constr] would shelve every
+created evar, which is not what we want, and it is hard to avoid since it
+happens very early (before we can easily wrap things in [unshelve]). *)
 Ltac opose_core p tac :=
-  (* If the user picked a name, this "fresh" runs *before* that name is in the
-  context, so we better make sure we do not use the name the user picked. *)
-  let i := fresh "opose" in
+  (* The "opose_internal" here is useful for debugging but not helpful for name
+  collisions since it gets ignored with name mangling. The [clear] below is what
+  ensures we don't get name collisions. *)
+  let i := fresh "opose_internal" in
   unshelve (epose _ as i);
     [shelve (*type of [p]*)
-    |refine p; shelve_unifiable (* will create the subgoals *)
-    |let t := eval cbv delta [i] in i in
+    |refine p (* will create the subgoals, and shelve some of them *)
+    |(* Now we have [i := t] in the context, let's get the [t] and remove [i]. *)
+     let t := eval unfold i in i in
+     (* We want to leave the context exactly as we found it, to avoid
+     any issues with fresh name generation. So clear [i] before calling
+     the user-visible tactic. *)
      clear i;
      tac t];
+  (* [tac] might have added more subgoals, making some existing ones
+  unifiable, so we need to shelve again. *)
   shelve_unifiable.
 
-Ltac ospecialize_foralls p tac :=
+(** Turn all leading ∀ and → of [p] into evars (∀-evars will be shelved), and
+call [tac] with the term applied with those evars. This fill unfold definitions
+to find leading ∀/→.
+
+[_name_guard] is an unused argument where you can pass anything you want. If the
+argument is an intro pattern, those will be taken into account by the [fresh]
+that is inside this tactic, avoiding name collisions that can otherwise arise.
+This is a work-around for https://github.com/coq/coq/issues/18109. *)
+Ltac ospecialize_foralls p _name_guard tac :=
   let T := type of p in
   lazymatch eval hnf in T with
   | ?T1 → ?T2 =>
-    (* Similar to [opose_core] we need to ensure freshness. *)
-    let pT1 := fresh "opose" in
-    assert T1 as pT1; [| ospecialize_foralls (p pT1) tac; clear pT1]
+    (* This is the [fresh] where the presence of [_name_guard] matters.
+    Note that the "opose_internal" is nice but not sufficient because
+    it gets ignored when name mangling is enabled. *)
+    let pT1 := fresh "opose_internal" in
+    assert T1 as pT1; [| ospecialize_foralls (p pT1) _name_guard tac; clear pT1]
   | ∀ x : ?T1, _ =>
     let e := mk_evar T1 in
-    ospecialize_foralls (p e) tac
+    ospecialize_foralls (p e) _name_guard tac
   | ?T1 => tac p
   end.
 
-Ltac opose_specialize_foralls_core p tac :=
-  opose_core p ltac:(fun p => ospecialize_foralls p tac).
+Ltac opose_specialize_foralls_core p _name_guard tac :=
+  opose_core p ltac:(fun p => ospecialize_foralls p _name_guard tac).
 
 Tactic Notation "opose" "proof" uconstr(p) "as" simple_intropattern(pat) :=
-  opose_core p ltac:(fun i => pose proof i as pat).
+  opose_core p ltac:(fun p => pose proof p as pat).
 Tactic Notation "opose" "proof" "*" uconstr(p) "as" simple_intropattern(pat) :=
-  opose_specialize_foralls_core p ltac:(fun i => pose proof i as pat).
+  opose_specialize_foralls_core p pat ltac:(fun p => pose proof p as pat).
 
 Tactic Notation "opose" "proof" uconstr(p) := opose proof p as ?.
 Tactic Notation "opose" "proof" "*" uconstr(p) := opose proof* p as ?.
 
 Tactic Notation "ogeneralize" uconstr(p) :=
-  opose_core p ltac:(fun i => generalize i).
+  opose_core p ltac:(fun p => generalize p).
 Tactic Notation "ogeneralize" "*" uconstr(p) :=
-  opose_specialize_foralls_core p ltac:(fun i => generalize i).
+  opose_specialize_foralls_core p () ltac:(fun p => generalize p).
 
 (** Similar to [edestruct], [odestruct] will never clear the destructed
 variable. *)
-(** No [*] versions for [odestruct] and [oinversion]; we always specialize all
-foralls and implications; otherwise it does not make sense to destruct/invert. *)
+(** No [*] versions for [odestruct] and [oinversion]: we always specialize all
+foralls and implications; otherwise it does not make sense to destruct/invert.
+We also do not support [eqn:EQ]; this would not make sense for most users of
+this tactic since the term being destructed is [some_lemma ?evar ?proofterm]. *)
+Tactic Notation "odestruct" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p => destruct p).
 Tactic Notation "odestruct" uconstr(p) "as" simple_intropattern(pat) :=
-  opose_specialize_foralls_core p ltac:(fun i => destruct i as pat).
+  opose_specialize_foralls_core p pat ltac:(fun p => destruct p as pat).
 
 Tactic Notation "oinversion" uconstr(p) "as" simple_intropattern(pat) :=
-  opose_specialize_foralls_core p ltac:(fun i =>
-    let Hi := fresh in pose proof i as Hi; inversion Hi as pat; clear Hi).
+  opose_specialize_foralls_core p pat ltac:(fun p =>
+    let Hp := fresh in pose proof p as Hp; inversion Hp as pat; clear Hp).
 Tactic Notation "oinversion" uconstr(p) :=
-  opose_specialize_foralls_core p ltac:(fun i =>
-    let Hi := fresh in pose proof i as Hi; inversion Hi; clear Hi).
+  opose_specialize_foralls_core p () ltac:(fun p =>
+    let Hp := fresh in pose proof p as Hp; inversion Hp; clear Hp).
+
+(** Helper for [ospecialize]: call [tac] with the name of the head term *if*
+that term is a variable.
 
+Written in CPS to get around weird thunking limitations. *)
 Ltac ospecialize_ident_head_of t tac :=
   let h := get_head t in
-  first
-    [is_var h
-    |fail 1 "ospecialize can only specialize a local hypothesis;"
-              "use opose proof instead"];
-  tac h.
+  tryif is_var h then tac h else
+    fail "ospecialize can only specialize a local hypothesis;"
+         "use opose proof instead".
 
 Tactic Notation "ospecialize" uconstr(p) :=
   (* Unfortunately there does not seem to be a way to reuse [specialize] here,
   so we need to re-implement the logic for reusing the name. *)
-  opose_core p ltac:(fun i =>
-    (* [i] is the name of a variable with value [p],
-       we need to get the value. *)
-    ospecialize_ident_head_of i ltac:(fun H =>
-      (* The body of [i] refers to [H] so it needs to be cleared first. *)
+  opose_core p ltac:(fun p =>
+    ospecialize_ident_head_of p ltac:(fun H =>
+      (* The term of [p] (but not its type) can refer to [H], so we need to use
+      a temporary [H'] here to hold the type of [p] before we can clear [H]. *)
       let H' := fresh in
-      pose proof i as H'; clear H; rename H' into H
+      pose proof p as H'; clear H; rename H' into H
   )).
 Tactic Notation "ospecialize" "*" uconstr(p) :=
-  opose_specialize_foralls_core p ltac:(fun i =>
-    ospecialize_ident_head_of i ltac:(fun H =>
+  opose_specialize_foralls_core p () ltac:(fun p =>
+    ospecialize_ident_head_of p ltac:(fun H =>
+      (* The term of [p] (but not its type) can refer to [H], so we need to use
+      a temporary [H'] here to hold the type of [p] before we can clear [H]. *)
       let H' := fresh in
-      pose proof i as H'; clear H; rename H' into H
+      pose proof p as H'; clear H; rename H' into H
   )).
 
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
diff --git a/tests/tactics.v b/tests/tactics.v
index 70254c9075bab79fa57d6147add347cf531236e7..5aa85fce19b5c197d02fe7f8d15fc776ad65cf04 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -1,4 +1,4 @@
-From stdpp Require Import tactics option.
+From stdpp Require Import tactics.
 
 Local Unset Mangle Names. (* for stable goal printing *)
 
@@ -84,11 +84,6 @@ Restart.
   - left. exact H2.
 Qed.
 
-(** Regression tests for [naive_solver]. *)
-Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
-  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
-Proof. naive_solver. Qed.
-
 (** [mk_evar] works on things that coerce to types. *)
 (** This is a feature when we have packed structures, for example Iris's [ofe]
 (fields other than the carrier omitted). *)
@@ -103,15 +98,6 @@ Goal True.
 let x := mk_evar true in idtac.
 Abort.
 
-(** Make sure that [done] is not called recursively when solving [is_Some],
-which might leave an unresolved evar before performing ex falso. *)
-Goal False → is_Some (@None nat).
-Proof. done. Qed.
-Goal ∀ mx, mx = Some 10 → is_Some mx.
-Proof. done. Qed.
-Goal ∀ mx, Some 10 = mx → is_Some mx.
-Proof. done. Qed.
-
 (** get_head tests. *)
 Lemma test_get_head (f : nat → nat → nat → nat) : True.
 Proof.
@@ -119,26 +105,6 @@ Proof.
   let f' := get_head f in unify f f'.
 Abort.
 
-Lemma o_tactic_without_forall (P Q R : Prop) :
-  P → Q → (P → Q → R) → R.
-Proof.
-  intros HP HQ HR.
-  ospecialize* HR; [exact HP|exact HQ|exact HR].
-Restart.
-  intros HP HQ HR.
-  opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
-Qed.
-
-Lemma o_tactic_with_forall (P Q R : nat → Prop) :
-  P 1 → Q 1 → (∀ n, P n → Q n → R n) → R 1.
-Proof.
-  intros HP HQ HR.
-  ospecialize* HR; [exact HP|exact HQ|exact HR].
-Restart.
-  intros HP HQ HR.
-  opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
-Qed.
-
 (** o-tactic tests *)
 (* Check "otest". *)
 Lemma otest (P Q R : nat → Prop)
@@ -153,20 +119,23 @@ Proof.
   a short proof script can solve them. [n] needs to be specified, but [m] is
   huge and we don't want to specify it. What do we do? The "o" family of tactics
   for working with "o"pen terms helps. *)
-  opose proof* (HPQR1 _ (S _)) as HR; [exact HP1|exact HQ|]. exact HR.
+  opose proof (HPQR1 _ (S _) _ _) as HR; [exact HP1|exact HQ|]. exact HR.
+Restart.
+  (** We can have fewer [_]. *)
+  opose proof (HPQR1 _ (S _) _) as HR; [exact HP1|]. exact (HR HQ).
 Restart.
-  (** If we omit the [*] no goals are created *)
+  (** And even fewer. *)
   opose proof (HPQR1 _ (S _)) as HR. exact (HR HP1 HQ).
 Restart.
-  (** If we want to specify how many goals we get, we can use [_]s. *)
-  opose proof (HPQR1 _ (S _) _) as HR; [exact HP1|]. exact (HR HQ).
+  (** The [*] variant automatically adds [_]. *)
+  opose proof* (HPQR1 _ (S _)) as HR; [exact HP1|exact HQ|]. exact HR.
 Restart.
   (** Same deal for [generalize]. *)
-  ogeneralize* (HPQR1 _ 1); [exact HP1|exact HQ|]. intros HR. exact HR.
-Restart.
   ogeneralize (HPQR1 _ 1). intros HR. exact (HR HP1 HQ).
 Restart.
   ogeneralize (HPQR1 _ 1 _); [exact HP1|]. intros HR. exact (HR HQ).
+Restart.
+  ogeneralize* (HPQR1 _ 1); [exact HP1|exact HQ|]. intros HR. exact HR.
 Restart.
   (** [odestruct] also automatically adds subgoals until there is something
   to destruct, as usual. Note that [edestruct] wouldn't help here,
@@ -176,10 +145,42 @@ Restart.
 Restart.
   (** [ospecialize] is like [opose proof] but it reuses the name.
   It only works on local assumptions. *)
-  Fail ospecialize (mk_is_Some None).
-  ospecialize* (HPQR1 _ 1); [exact HP1|exact HQ|]. exact HPQR1.
+  Fail ospecialize (plus 0 0).
+  ospecialize (HPQR1 _ 1 _); [exact HP1|]. exact (HPQR1 HQ).
 Restart.
   ospecialize (HPQR1 _ 1). exact (HPQR1 HP1 HQ).
 Restart.
-  ospecialize (HPQR1 _ 1 _); [exact HP1|]. exact (HPQR1 HQ).
+  ospecialize* (HPQR1 _ 1); [exact HP1|exact HQ|]. exact HPQR1.
 Qed.
+
+(** Make sure [∀] also get auto-instantiated by the [*] variant. *)
+Lemma o_tactic_with_forall (P Q R : nat → Prop) :
+  P 1 → Q 1 → (∀ n, P n → Q n → R n) → R 1.
+Proof.
+  intros HP HQ HR.
+  ospecialize* HR; [exact HP|exact HQ|exact HR].
+Restart.
+  intros HP HQ HR.
+  opose proof* HR as HR'; [exact HP|exact HQ|exact HR'].
+Qed.
+
+(** Now that we have seen that the basic tactics are working,
+we are okay importing some other files. We don't want to do this
+above since it can make debugging hard: if a tactic breaks,
+[option] breaks, and then we cannot even use the tests here to figure out
+what is going on! *)
+From stdpp Require Import option.
+
+(** Make sure that [done] is not called recursively when solving [is_Some],
+which might leave an unresolved evar before performing ex falso. *)
+Goal False → is_Some (@None nat).
+Proof. done. Qed.
+Goal ∀ mx, mx = Some 10 → is_Some mx.
+Proof. done. Qed.
+Goal ∀ mx, Some 10 = mx → is_Some mx.
+Proof. done. Qed.
+
+(** Regression tests for [naive_solver]. *)
+Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
+  (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
+Proof. naive_solver. Qed.