fix compilation wrt. commit 699b70c in Coq trunk

1 files changed, 7 insertions, 7 deletions

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 6559504..1250f7e 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -52,7 +52,7 @@ open Tacexpr
 open Tacinterp
 open Pretyping
 open Constr
-open Tactic
+open Pltac
 open Extraargs
 open Ppconstr
 open Printer
@@ -471,7 +471,7 @@ let _ =
       Goptions.optwrite = (fun _ -> 
         Lib.add_anonymous_leaf (inVersion ssrAstVersion)) }
 
-let tactic_expr = Tactic.tactic_expr
+let tactic_expr = Pltac.tactic_expr
 let gallina_ext = Vernac_.gallina_ext 
 let sprintf = Printf.sprintf
 let tactic_mode = G_ltac.tactic_mode
@@ -5703,7 +5703,7 @@ ARGUMENT EXTEND ssrhavefwdwbinders
     tr, ((((clr, pats), allbinders), simpl), hint) ]
 END
 
-(* Tactic. *)
+(* Pltac. *)
 
 let is_Evar_or_CastedMeta x =
   isEvar_or_Meta x ||
@@ -6205,8 +6205,8 @@ END
 (* longer and thus comment out. Such comments are marked with v8.3     *)
 
 GEXTEND Gram
-  GLOBAL: Tactic.hypident;
-  Tactic.hypident: [
+  GLOBAL: Pltac.hypident;
+  Pltac.hypident: [
   [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
   | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
   ] ];
@@ -6223,8 +6223,8 @@ hloc: [
 END
 
 GEXTEND Gram
-  GLOBAL: Tactic.constr_eval;
-  Tactic.constr_eval: [
+  GLOBAL: Pltac.constr_eval;
+  Pltac.constr_eval: [
     [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
   ];
 END