Fixes #10778 (fresh was not updated after renaming of intropattern entry in #10239).

The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.

We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).

3 files changed, 35 insertions, 6 deletions

diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 9e8e86d4fc..252c15478d 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -20,7 +20,7 @@ let make0 ?dyn name =
   wit
 
 let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *)
-let wit_simple_intropattern = make0 "simple_intropattern"
+let wit_simple_intropattern = make0 ~dyn:(val_tag (topwit wit_intropattern)) "simple_intropattern"
 let wit_quant_hyp = make0 "quant_hyp"
 let wit_constr_with_bindings = make0 "constr_with_bindings"
 let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index e64129d204..da89a027e2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -145,11 +145,8 @@ let coerce_to_constr_context v =
   else raise (CannotCoerceTo "a term context")
 
 let is_intro_pattern v =
-  if has_type v (topwit wit_intropattern [@warning "-3"]) then
-    Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v
-  else
-  if has_type v (topwit wit_simple_intropattern) then
-    Some (out_gen (topwit wit_simple_intropattern) v).CAst.v
+  if has_type v (topwit wit_intro_pattern) then
+    Some (out_gen (topwit wit_intro_pattern) v).CAst.v
   else
     None
 
diff --git a/test-suite/bugs/closed/bug_10778.v b/test-suite/bugs/closed/bug_10778.v
new file mode 100644
index 0000000000..25d729b7e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10778.v
@@ -0,0 +1,32 @@
+(* Test that fresh avoid the variables of intro patterns but also of
+   simple intro patterns *)
+
+Ltac exploit_main t T pat cleanup
+  :=
+  (lazymatch T with
+   | ?U1 -> ?U2 =>
+       let H := fresh
+       in
+idtac "H=" H;
+         assert U1 as H;
+         [cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
+   | _ =>
+       pose proof t as pat;
+       cleanup ()
+   end).
+
+Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit H0 as H.
+Abort.
+
+Tactic Notation "exploit'" constr(t) "as" intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit' H0 as H.
+Abort.