updated to 8.5

test-suite/mtactest.v

@@ -18,9 +18,9 @@ Goal True.
   rrun (ret I).
 Qed.
 
-Definition test_of_definition : nat := $( rrun (ret 0) )$.
+Definition test_of_definition : nat := ltac:( rrun (ret 0) ).
 
-Definition test_of_definition_evar  : 0 = 0 := $( rrun (ret (eq_refl _)) )$.
+Definition test_of_definition_evar  : 0 = 0 := ltac:( rrun (ret (eq_refl _)) ).
 
 
 Definition MyException (x:nat) : Exception. exact exception. Qed.
@@ -47,7 +47,7 @@ Definition abs_evar (A : Type) :=
   f <- @abs Type (fun A'=>A') A e  : M (forall A : Type, A);
   ret (f nat, f bool).
 
-Check (fun A : Type => $( rrun (abs_evar A) )$ ). 
+Check (fun A : Type => ltac:( rrun (abs_evar A) ) ). 
 
 Definition abs_val2 (A : Type) :=
   e <- evar A;

test-suite/testmtactics.v

@@ -66,8 +66,8 @@ Section TestMmatch'.
 
 
 Time Example test_this_dainlist (x y z : nat) : In x ([z;z;z;z;z;z;y]++[z;y;x]) := 
-  $( rrun (dainlist _ _) )$.
+  ltac:( rrun (dainlist _ _) ).
 Time Example test_this_inlist (x y z : nat) : In x ([z;z;z;z;z;z;y]++[z;y;x]) := 
-  $( rrun (ListMtactics.inlist _ _) )$.
+  ltac:( rrun (ListMtactics.inlist _ _) ).
 
 End TestMmatch'.

theories/Mtac.v

@@ -152,7 +152,7 @@ Arguments runner {A} _.
 Arguments Build_runner {A} _ _.
 Arguments eval {A} _ {_}.
 
-Hint Extern 20 (runner ?f) => (exact (Build_runner f $(rrun f)$))  : typeclass_instances.
+Hint Extern 20 (runner ?f) => (exact (Build_runner f ltac:(rrun f)))  : typeclass_instances.
 
 (*
 Definition lift {A} (f : Mtac A) (v : A) := A.
@@ -176,7 +176,7 @@ Export Mtac.
 
 Module MtacNotations.
 
-Notation "'Mrun' t" := ($( rrun t )$) (at level 0).
+Notation "'Mrun' t" := (ltac:(rrun t)) (at level 0).
 
 Notation "'M'" := Mtac.
 

theories/Mtactics.v

@@ -158,8 +158,8 @@ Proof. tauto. Qed.
 
 
 Program Definition tauto0 :=
-  mfix1 f (P : Prop) : M P :=
-    mmatch P as P' return M P' with
+  mfix1 f (P : Prop) : M (P : Prop) :=
+    mmatch P as P' return M (P' : Prop) with
     | True => ret I
     | [? R Q] R /\ Q =>
       r1 <- f R;
@@ -269,7 +269,7 @@ Set Printing Universes.
 Definition match_goal {A:Type} {P:A->Type} (t : A) (p : tpatt A P t) 
 : M (list dyn * P t) :=
   pes <- eopen_pattern p [];
-  let (ls, goal) := pes : (list dyn@{i} * tpatt _ _ _)%type in
+  let (ls, goal) := pes : (list dyn * tpatt _ _ _)%type in
   mmatch goal with
   | [? f u] @base A P t t f u => 
     pf <- (f eq_refl) : M (P t);

tutorial/mtac_tutorial.v

@@ -319,7 +319,7 @@ application of the tactic [rrun] with the [$(...)$] extension in Coq 8.5
 to use tactics to build terms. *)
 
 Example z_in_xyz (x y z : nat) : In z (x :: y :: z :: nil)
-  := $(rrun (inlist _ _))$.
+  := ltac:(rrun (inlist _ _)).
 
 (** An alternative is to use [eval], which is similar to [Mrun], except
 that it performs the execution of the Mtactic after the type inference
@@ -454,8 +454,8 @@ only three cases:
 *)
 
 Definition simpl_prop_auto :=
-  mfix1 f (p : Prop) : M p :=
-    mmatch p as p' return M p' with
+  mfix1 f (p : Prop) : M (p : Prop) :=
+    mmatch p as p' return M (p':Prop) with
     | True => ret I 
     | [? p1 p2 ] p1 /\ p2 =>
          r1 <- f p1 ;
@@ -517,7 +517,7 @@ and a proposition. The first three cases are the same as before.  *)
 
 Definition prop_auto' :=
   mfix2 f (c : list dyn) (p : Prop) : M p :=
-    mmatch p as p' return M p' with
+    mmatch p as p' return M (p':Prop) with
     | True => ret I 
     | [? p1 p2 ] p1 /\ p2 =>
          r1 <- f c p1 ;
@@ -606,7 +606,7 @@ are the same as before. *)
 
 Definition tauto' :=
   mfix2 f (c : list dyn) (p : Prop) : M p :=
-    mmatch p as p' return M p' with
+    mmatch p as p' return M (p':Prop) with
     | True => ret I 
     | [? p1 p2] p1 /\ p2 =>
          r1 <- f c p1 ;