1 files changed, 7 insertions, 6 deletions
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index b6523981c..16934fc86 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -12,6 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Glob_term
 open Vernacexpr
 open Constrexpr
 open Constrexpr_ops
@@ -19,7 +20,7 @@ open Extend
 open Decl_kinds
 open Declaremods
 open Declarations
-open Misctypes
+open Namegen
 open Tok (* necessary for camlp5 *)
 
 open Pcoq
@@ -338,7 +339,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
+      | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -394,7 +395,7 @@ GEXTEND Gram
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
+    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -413,7 +414,7 @@ GEXTEND Gram
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+                 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ]
 	 -> t l
      ]]
 ;
@@ -548,7 +549,7 @@ GEXTEND Gram
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -558,7 +559,7 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid
       | "("; mt = module_type; ")" -> mt
       | mty = module_type; me = module_expr_atom ->
           CAst.make ~loc:!@loc @@ CMapply (mty,me)