Merge branch 'v8.5'

5 files changed, 10 insertions, 10 deletions

diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 9e7d1eb5d..33c408a28 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/3248.v
@@ -3,7 +3,7 @@ Ltac ret_and_left f :=
   let T := type of f in
   lazymatch eval hnf in T with
     | ?T' -> _ =>
-      let ret := constr:(fun x' : T' => $(tac (f x'))$) in
+      let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in
       exact ret
     | ?T' => exact f
   end.
@@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True.
 Proof.
   intros A B x y.
   pose (f := fun (x y : A) => conj x y).
-  pose (a := $(ret_and_left f)$).
+  pose (a := ltac:(ret_and_left f)).
   Fail unify (a x y) (conj x y).
 Abort.
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v
index 19ed787d1..5f4231363 100644
--- a/test-suite/bugs/opened/3277.v
+++ b/test-suite/bugs/opened/3277.v
@@ -4,4 +4,4 @@ Goal True.
   evarr _.
 Admitted.
 Goal True.
-  Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *)
+  Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
index ced535afd..1c6deae94 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/3278.v
@@ -1,8 +1,8 @@
 Module a.
   Check let x' := _ in
-             $(exact x')$.
+             ltac:(exact x').
 
-  Notation foo x := (let x' := x in $(exact x')$).
+  Notation foo x := (let x' := x in ltac:(exact x')).
 
   Fail Check foo _. (* Error:
 Cannot infer an internal placeholder of type "Type" in environment:
@@ -12,10 +12,10 @@ x' := ?42 : ?41
 End a.
 
 Module b.
-  Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
+  Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I).
   Notation bar x := (let x' := x in let y := (I : True) in I).
 
-  Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *)
+  Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *)
   Check bar _. (* let x' := ?9 in let y := I in I *)
   Fail Check foo _. (* Error:
 Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v
index 529cc737d..66668930c 100644
--- a/test-suite/bugs/opened/3304.v
+++ b/test-suite/bugs/opened/3304.v
@@ -1,3 +1,3 @@
-Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$.
+Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r).
 (* The command has indeed failed with message:
 => Error: Special token .. is for use in the Notation command. *)
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index 9e6107b30..762611f75 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -7,9 +7,9 @@ Proof.
 (* This line used to fail with a Not_found up to some point, and then
    to produce an ill-typed term *)
 match goal with
-  | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in
+  | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in
                                                        clear x;
-                                                       exact r)$) in
+                                                       exact r)) in
                            pose y
 end.
 (* Add extra test for typability (should not fail when bug closed) *)