Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 580 insertions, 361 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 87183e18..18a424a8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,35 +6,39 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_vernac.ml4,v 1.93.2.3 2004/10/12 10:11:28 herbelin Exp $ *)
+(* $Id: g_vernac.ml4 8624 2006-03-13 17:38:17Z msozeau $ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
+open Pp
+open Util
 open Names
 open Topconstr
 open Vernacexpr
 open Pcoq
-open Pp
 open Tactic
-open Util
-open Constr
-open Vernac_
-open Prim
 open Decl_kinds
-
 open Genarg
+open Extend
+open Ppextend
+open Goptions
 
-let evar_constr loc = CHole loc
+open Prim
+open Constr
+open Vernac_
+open Module
 
-let class_rawexpr = G_basevernac.class_rawexpr
-let thm_token = G_proofs.thm_token
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
+let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let filter_com (b,e) =
-  let (b,e) = unloc (b,e) in
-  Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments 
+let check_command = Gram.Entry.create "vernac:check_command"
+let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
+let thm_token = Gram.Entry.create "vernac:thm_token"
+let def_body = Gram.Entry.create "vernac:def_body"
 
-if !Options.v7 then
+let no_hook _ _ = ()
 GEXTEND Gram
   GLOBAL: vernac gallina_ext;
   vernac:
@@ -44,163 +48,121 @@ GEXTEND Gram
       | g = gallina_ext; "." -> g
       | c = command; "." -> c 
       | c = syntax; "." -> c
-      | n = natural; ":"; tac = Tactic.tactic; "." -> VernacSolve (n,tac,true) 
-      | n = natural; ":"; tac = Tactic.tactic; "!!" -> VernacSolve (n,tac,false)
-      | n = natural; ":"; v = check_command; "." -> v (Some n)
-      | "["; l = vernac_list_tail -> VernacList l
-
-      (* For translation from V7 to V8 *)
-      | IDENT "V7only"; v = vernac ->
-          filter_com loc; VernacV7only v
-      | IDENT "V8only"; v = vernac -> VernacV8only v
-
-(*
-      (* This is for "Grammar vernac" rules *)
-      | id = METAIDENT -> VernacVar (Names.id_of_string id)
-*)
+      | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
     ] ]
   ;
-    
-  check_command:
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr ->
-          fun g -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Check"; c = constr ->
-	  fun g -> VernacCheckMayEval (None, g, c) ] ]
-  ;
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
   ;
   vernac: LAST
-    [ [ tac = Tactic.tactic; "." -> VernacSolve (1,tac,true)
-      | tac = Tactic.tactic; "!!" -> VernacSolve (1,tac,false)
-      | IDENT "Existential"; n = natural; c = constr_body ->
-	  VernacSolveExistential (n,c)
-    ] ]
-  ;
-  constr_body:
-    [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t)
-      | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t)
-      | ":="; c = constr -> c ] ]
+    [ [ gln = OPT[n=natural; ":" -> n];
+        tac = subgoal_command -> tac gln ] ]
   ;
-  vernac_list_tail:
-    [ [ v = located_vernac; l = vernac_list_tail -> v :: l
-      | "]"; "." -> [] ] ]
+  subgoal_command:
+    [ [ c = check_command; "." -> c
+      | tac = Tactic.tactic;
+        use_dft_tac = [ "." -> false | "..." -> true ] ->
+          (fun g ->
+            let g = match g with Some gl -> gl | _ -> 1 in
+            VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
   ;
 END
 
+
 let test_plurial_form = function
-  | [_,([_],_)] ->
+  | [(_,([_],_))] ->
       Options.if_verbose warning
-      "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
+   "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
 
+let no_coercion loc (c,x) =
+  if c then Util.user_err_loc
+    (loc,"no_coercion",Pp.str"no coercion allowed here");
+  x
+
 (* Gallina declarations *)
-if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: gallina gallina_ext thm_token;
+  GLOBAL: gallina gallina_ext thm_token def_body;
 
+  gallina:
+      (* Definition, Theorem, Variable, Axiom, ... *)
+    [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":";
+        c = lconstr ->
+          VernacStartTheoremProof (thm, id, (bl, c), false, no_hook)
+      | stre = assumption_token; bl = assum_list -> 
+	  VernacAssumption (stre, bl)
+      | stre = assumptions_token; bl = assum_list ->
+	  test_plurial_form bl;
+	  VernacAssumption (stre, bl)
+      | IDENT "Boxed";"Definition";id = identref; b = def_body -> 
+	  VernacDefinition ((Global,true,Definition), id, b, no_hook)
+      | IDENT "Unboxed";"Definition";id = identref; b = def_body -> 
+	  VernacDefinition ((Global,false,Definition), id, b, no_hook)
+      | (f,d) = def_token; id = identref; b = def_body -> 
+          VernacDefinition (d, id, b, f)
+      (* Gallina inductive declarations *)
+      | f = finite_token;
+        indl = LIST1 inductive_definition SEP "with" ->
+          VernacInductive (f,indl)
+      | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (recs,true)
+      | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (recs,false)
+       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (recs,Options.boxed_definitions())
+      | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (corecs,false)
+      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
+  ;
+  gallina_ext:
+    [ [ b = record_token; oc = opt_coercion; name = identref;
+        ps = LIST0 binder_let; ":";
+	s = lconstr; ":="; cstr = OPT identref; "{";
+        fs = LIST0 record_field SEP ";"; "}" ->
+	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
+(* Non port�é ?
+      | f = finite_token; s = csort; id = identref;
+        indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
+          VernacInductive (f,[id,None,indpar,s,lc])
+*)
+    ] ]
+  ;
   thm_token:
     [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
-      | IDENT "Remark" -> Remark ] ]
+      | IDENT "Remark" -> Remark
+      | IDENT "Corollary" -> Corollary
+      | IDENT "Proposition" -> Proposition
+      | IDENT "Property" -> Property ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
-      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition)
-      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
+    [ [ "Definition" -> 
+	no_hook, (Global, Options.boxed_definitions(), Definition)
+      | IDENT "Let" -> 
+	no_hook, (Local, Options.boxed_definitions(), Definition)
+      | IDENT "Example" -> 
+	no_hook, (Global, Options.boxed_definitions(), Example)
+      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, false, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
-	  Class.add_subclass_hook, (Local, SubClass) ] ] 
+          Class.add_subclass_hook, (Local, false, SubClass) ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
       | "Variable" -> (Local, Definitional)
       | "Axiom" -> (Global, Logical)
       | "Parameter" -> (Global, Definitional)
-      | IDENT "Conjecture" -> (Global,Conjectural) ] ]
+      | IDENT "Conjecture" -> (Global, Conjectural) ] ]
   ;
   assumptions_token:
     [ [ IDENT "Hypotheses" -> (Local, Logical)
       | IDENT "Variables" -> (Local, Definitional)
+      | IDENT "Axioms" -> (Global, Logical)
       | IDENT "Parameters" -> (Global, Definitional) ] ]
   ;
-  of_type_with_opt_coercion:
-    [ [ ":>" -> true
-      | ":"; ">" -> true
-      | ":" -> false ] ]
-  ;
-  params:
-    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; 
-        c = constr -> (coe,(idl,c))
-    ] ]
-  ;
-  ne_params_list:
-    [ [ ll = LIST1 params SEP ";" -> ll ] ]
-  ;
-  name_comma_list_tail:
-    [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
-  ;
-  ident_comma_list_tail:
-    [ [ ","; nal = LIST1 identref SEP "," -> nal | -> [] ] ]
-  ;
-  decl_notation:
-    [ [ "where"; ntn = STRING; ":="; c = constr; 
-         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ]
-  ;
-  type_option:
-    [ [ ":"; c = constr -> c 
-      | -> evar_constr loc ] ]
-  ;
-  opt_casted_constr:
-    [ [ c = constr;  ":"; t = constr -> CCast(loc,c,t)
-      | c = constr -> c ] ]
-  ;
-  vardecls:
-    [ [ na = name; nal = name_comma_list_tail; c = type_option
-          -> LocalRawAssum (na::nal,c)
-      | na = name; "="; c = opt_casted_constr ->
-          LocalRawDef (na,c)
-      | na = name; ":="; c = opt_casted_constr ->
-          LocalRawDef (na,c)
-    ] ]
-  ;
-  binders:
-    [ [ "["; bl = LIST1 vardecls SEP ";"; "]" -> bl ] ]
-  ;
-  binders_list:
-    [ [ bls = LIST0 binders -> List.flatten bls ] ]
-  ;
-  reduce:
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
-      | -> None ] ]
-  ;
-  def_body:
-    [ [ bl = binders_list; ":="; red = reduce; c = constr; ":"; t = constr ->
-          DefineBody (bl, red, c, Some t)
-      | bl = binders_list; ":"; t = constr; ":="; red = reduce; c = constr ->
-          DefineBody (bl, red, c, Some t)
-      | bl = binders_list; ":="; red = reduce; c = constr ->
-          DefineBody (bl, red, c, None)
-      | bl = binders_list; ":"; t = constr ->
-          ProveBody (bl, t) ] ]
-  ;
-  gallina:
-    (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders_list; ":"; c = constr ->
-         VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
-      | (f,d) = def_token; id = identref; b = def_body -> 
-          VernacDefinition (d, id, b, f)
-      | stre = assumption_token; bl = ne_params_list -> 
-	  VernacAssumption (stre, bl)
-      | stre = assumptions_token; bl = ne_params_list ->
-	  test_plurial_form bl;
-	  VernacAssumption (stre, bl)
-      ] ]
-  ;
-  (* Gallina inductive declarations *)
   finite_token:
     [ [ "Inductive" -> true
       | "CoInductive" -> false ] ]
@@ -208,192 +170,250 @@ GEXTEND Gram
   record_token:
     [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
   ;
-  constructor:
-    [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion;
-        c = constr -> List.map (fun id -> (coe,(id,c))) idl ] ]
-  ;
-  constructor_list:
-    [ [ "|"; l = LIST1 constructor SEP "|" -> List.flatten l
-      | l = LIST1 constructor SEP "|" -> List.flatten l
-      |  -> [] ] ]
-  ;
-  block_old_style:
-    [ [ ind = oneind_old_style; "with"; indl = block_old_style -> ind :: indl
-      | ind = oneind_old_style -> [ind] ] ]
+  (* Simple definitions *)
+  def_body:
+    [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr ->
+      (match c with
+          CCast(_,c,k,t) -> DefineBody (bl, red, c, Some t)
+        | _ -> DefineBody (bl, red, c, None))
+      | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = LIST0 binder_let; ":"; t = lconstr ->
+          ProveBody (bl, t) ] ]
   ;
-  oneind_old_style:
-    [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list ->
-          (id,c,lc) ] ]
+  reduce:
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
+      | -> None ] ]
   ;
-  oneind:
-    [ [ id = identref; indpar = simple_binders_list; ":"; c = constr; 
-        ":="; lc = constructor_list; ntn = OPT decl_notation ->
+  decl_notation:
+    [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr; 
+         scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ]
+    ;
+  (* Inductives and records *)
+  inductive_definition:
+    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; 
+        ":="; lc = constructor_list; ntn = decl_notation ->
 	  (id,ntn,indpar,c,lc) ] ]
   ;
-  simple_binders_list:
-    [ [ bl = ne_simple_binders_list -> bl
+  constructor_list:
+    [ [ "|"; l = LIST1 constructor SEP "|" -> l
+      | l = LIST1 constructor SEP "|" -> l
       |  -> [] ] ]
   ;
+(*
+  csort:
+    [ [ s = sort -> CSort (loc,s) ] ]
+  ;
+*)
   opt_coercion:
     [ [ ">" -> true
       |  -> false ] ]
   ;
-  onescheme:
-    [ [ id = identref; ":="; dep = dep; ind = global; IDENT "Sort";
-        s = sort -> (id,dep,ind,s) ] ]
-  ;
-  schemes:
-    [ [ recl = LIST1 onescheme SEP "with" -> recl ] ]
-  ;
-  dep:
-    [ [ IDENT "Induction"; IDENT "for" -> true
-      | IDENT "Minimality"; IDENT "for" -> false ] ]
+  (* (co)-fixpoints *)
+  rec_definition:
+    [ [ id = ident; bl = LIST1 binder_let;
+        annot = rec_annotation; type_ = type_cstr; 
+	":="; def = lconstr; ntn = decl_notation ->
+          let names = List.map snd (names_of_local_assums bl) in
+          let ni =
+            match fst annot with
+                Some id ->
+                  (try list_index (Name id) names - 1
+                  with Not_found ->  Util.user_err_loc
+                      (loc,"Fixpoint",
+                       Pp.str "No argument named " ++ Nameops.pr_id id))
+              | None -> 
+                  if List.length names > 1 then
+                    Util.user_err_loc
+                      (loc,"Fixpoint",
+                       Pp.str "the recursive argument needs to be specified");
+                  0 in
+	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
+  ;
+  corec_definition:
+    [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
+        def = lconstr ->
+          (id,bl,c ,def) ] ]
+  ;
+  rec_annotation:
+    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
+      | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | ->  (None, CStructRec)
+      ] ]
   ;
-  onerec:
-    [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
-        ":="; def = constr; ntn = OPT decl_notation ->
-          let ni = List.length (List.flatten (List.map fst bl)) - 1 in
-          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
-	  ((id, ni, bl, type_, def), ntn) ] ]
+  type_cstr:
+    [ [ ":"; c=lconstr -> c 
+      | -> CHole loc ] ]
   ;
-  specifrec:
-    [ [ l = LIST1 onerec SEP "with" -> l ] ]
+  (* Inductive schemes *)
+  scheme:
+    [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global;
+        IDENT "Sort"; s = sort ->
+          (id,dep,ind,s) ] ]
   ;
-  onecorec:
-    [ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
-          (id,[],c,def) ] ]
+  dep_scheme:
+    [ [ IDENT "Induction" -> true
+      | IDENT "Minimality" -> false ] ]
   ;
-  specifcorec:
-    [ [ l = LIST1 onecorec SEP "with" -> l ] ]
+  (* Various Binders *)
+(*
+  (* ... without coercions *)
+  binder_nodef:
+    [ [ b = binder_let ->
+      (match b with
+          LocalRawAssum(l,ty) -> (l,ty)
+        | LocalRawDef _ ->
+            Util.user_err_loc
+              (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ]
   ;
+*)
+  (* ... with coercions *)
   record_field:
-    [ [ id = name; oc = of_type_with_opt_coercion; t = constr ->
-          (oc,AssumExpr (id,t))
-      | id = name; oc = of_type_with_opt_coercion; t = constr;
-	":="; b = constr ->
-	  (oc,DefExpr (id,b,Some t))
-      | id = name; ":="; b = constr ->
-	  (false,DefExpr (id,b,None)) ] ]
-  ;
-  fields:
-    [ [ fs = LIST0 record_field SEP ";" -> fs ] ]
-  ;
-  simple_binders:
-    [ [ "["; bll = LIST1 vardecls SEP ";"; "]" -> bll ] ]
-  ;
-  ne_simple_binders_list:
-    [ [ bll = LIST1 simple_binders -> (List.flatten bll) ] ]
-  ;
-  fix_params:
-    [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
-      | idl = LIST1 name SEP "," -> (idl, evar_constr dummy_loc)
-    ] ]
-  ;
-  fix_binders:
-    [ [ "["; bll = LIST1 fix_params SEP ";"; "]" -> bll ] ]
-  ;
-  ne_fix_binders:
-    [ [ bll = LIST1 fix_binders -> List.flatten bll ] ]
+    [ [ id = name -> (false,AssumExpr(id,CHole loc))
+      | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
+         (oc,AssumExpr (id,t))
+      | id = name; oc = of_type_with_opt_coercion;
+             t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
+      | id = name; ":="; b = lconstr ->
+         match b with
+             CCast(_,b,_,t) -> (false,DefExpr(id,b,Some t))
+           | _ -> (false,DefExpr(id,b,None)) ] ]
+  ;
+  assum_list:
+    [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ]
+  ;
+  assum_coe:
+    [ [ "("; a = simple_assum_coe; ")" -> a ] ]
+  ;
+  simple_assum_coe:
+    [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> 
+        (oc,(idl,c)) ] ]
   ;
-  rec_constructor:
-    [ [ c = identref -> Some c
-      |  -> None ] ]
-  ;
-  gallina_ext:
-    [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
-        indl = block_old_style ->
-	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
-	  VernacInductive (f,indl')
-      | b = record_token; oc = opt_coercion; name = identref;
-	ps = simple_binders_list; ":";
-	s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
-	  VernacRecord (b,(oc,name),ps,s,c,fs)
-    ] ]
-  ;
-  gallina:
-    [ [ IDENT "Mutual"; f = finite_token; indl = LIST1 oneind SEP "with" ->
-          VernacInductive (f,indl)
-      | f = finite_token; indl = LIST1 oneind SEP "with" ->
-          VernacInductive (f,indl)
-      | "Fixpoint"; recs = specifrec -> VernacFixpoint recs
-      | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
-      | IDENT "Scheme"; l = schemes -> VernacScheme l
-      | f = finite_token; s = csort; id = identref;
-	indpar = simple_binders_list; ":="; lc = constructor_list -> 
-          VernacInductive (f,[id,None,indpar,s,lc]) ] ]
+  constructor:
+    [ [ id = identref; l = LIST0 binder_let; 
+        coe = of_type_with_opt_coercion; c = lconstr ->
+	  (coe,(id,G_constr.mkCProdN loc l c))
+      | id = identref; l = LIST0 binder_let ->
+	  (false,(id,G_constr.mkCProdN loc l (CHole loc))) ] ]
   ;
-  csort:
-    [ [ s = sort -> CSort (loc,s) ] ]
+  of_type_with_opt_coercion:
+    [ [ ":>" -> true
+      | ":"; ">" -> true
+      | ":" -> false ] ]
   ;
+END
+
+
+(* Modules and Sections *)
+GEXTEND Gram
+  GLOBAL: gallina_ext module_expr module_type;
+
   gallina_ext:
-    [ [ 
-(* Sections *)
-	IDENT "Section"; id = identref -> VernacBeginSection id
-      | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ]
-  ;
-  module_vardecls:
-    [ [ id = identref; idl = ident_comma_list_tail; ":";
-        mty = Module.module_type -> (id::idl,mty) ] ]
+    [ [ (* Interactive module declaration *)
+        IDENT "Module"; export = export_token; id = identref; 
+	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDefineModule (export, id, bl, mty_o, mexpr_o)
+	  
+      | IDENT "Module"; "Type"; id = identref; 
+	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
+	  VernacDeclareModuleType (id, bl, mty_o)
+	  
+      | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; 
+	bl = LIST0 module_binder; mty_o = of_module_type ->
+	  VernacDeclareModule (export, id, bl, mty_o)
+      (* Section beginning *)
+      | IDENT "Section"; id = identref -> VernacBeginSection id
+      | IDENT "Chapter"; id = identref -> VernacBeginSection id
+
+      (* This end a Section a Module or a Module Type *)
+      | IDENT "End"; id = identref -> VernacEndSegment id
+
+      (* Requiring an already compiled module *)
+      | IDENT "Require"; export = export_token; specif = specif_token;
+        qidl = LIST1 global ->
+          VernacRequire (export, specif, qidl)
+      | IDENT "Require"; export = export_token; specif = specif_token;
+        filename = ne_string -> 
+	  VernacRequireFrom (export, specif, filename)
+      | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
+      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ]
   ;
-  module_binders:
-    [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ]
+  export_token:
+    [ [ IDENT "Import" -> Some false
+      | IDENT "Export" -> Some true
+      |  -> None ] ]
   ;
-  module_binders_list:
-    [ [ bls = LIST0 module_binders -> List.flatten bls ] ]
+  specif_token:
+    [ [ IDENT "Implementation" -> Some false
+      | IDENT "Specification" -> Some true
+      |  -> None ] ]
   ;
   of_module_type:
-    [ [ ":"; mty = Module.module_type -> (mty, true) 
-      | "<:"; mty = Module.module_type -> (mty, false) ] ]
+    [ [ ":"; mty = module_type -> (mty, true) 
+      | "<:"; mty = module_type -> (mty, false) ] ]
   ;
   is_module_type:
-    [ [ ":="; mty = Module.module_type -> mty ] ]
+    [ [ ":="; mty = module_type -> mty ] ]
   ;
   is_module_expr:
-    [ [ ":="; mexpr = Module.module_expr -> mexpr ] ]
+    [ [ ":="; mexpr = module_expr -> mexpr ] ]
   ;
-  gallina_ext:
-    [ [ 
-	  (* Interactive module declaration *)
-	IDENT "Module"; id = identref; 
-	bl = module_binders_list; mty_o = OPT of_module_type; 
-	mexpr_o = OPT is_module_expr ->
-	  VernacDefineModule (id, bl, mty_o, mexpr_o)
-	  
-      | IDENT "Module"; "Type"; id = identref; 
-	bl = module_binders_list; mty_o = OPT is_module_type ->
-	  VernacDeclareModuleType (id, bl, mty_o)
-	  
-      | IDENT "Declare"; IDENT "Module"; id = identref; 
-	bl = module_binders_list; mty_o = OPT of_module_type; 
-	mexpr_o = OPT is_module_expr ->
-	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
 
-	  (* This end a Section a Module or a Module Type *)
+  (* Module binder  *)
+  module_binder:
+    [ [ "("; export = export_token; idl = LIST1 identref; ":";
+         mty = module_type; ")" -> (export,idl,mty) ] ]
+  ;
 
-      | IDENT "End"; id = identref -> VernacEndSegment id
+  (* Module expressions *)
+  module_expr:
+    [ [ qid = qualid -> CMEident qid
+      | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2)
+      | "("; me = module_expr; ")" -> me
+(* ... *)
+      ] ]
+  ;
+  with_declaration:
+    [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
+          CWith_Definition (fqid,c)
+      | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
+	  CWith_Module (fqid,qid)
+      ] ]
+  ;
+  module_type:
+    [ [ qid = qualid -> CMTEident qid
+(* ... *)
+      | mty = module_type; "with"; decl = with_declaration -> 
+	  CMTEwith (mty,decl) ] ]
+  ;
+END
 
+(* Extensions: implicits, coercions, etc. *)   
+GEXTEND Gram
+  GLOBAL: gallina_ext;
 
-(* Transparent and Opaque *)
-      | IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
+  gallina_ext:
+    [ [ (* Transparent and Opaque *)
+        IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
       | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l)
 
-(* Canonical structure *)
+      (* Canonical structure *)
       | IDENT "Canonical"; IDENT "Structure"; qid = global ->
 	  VernacCanonical qid
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
-          let s = Ast.coerce_global_to_id qid in
+          let s = coerce_global_to_id qid in
 	  VernacDefinition 
-	    ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
-      (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
-         (they were unused and undocumented) *)
+	    ((Global,false,CanonicalStructure),(dummy_loc,s),d,
+	     (fun _ -> Recordops.declare_canonical_structure))
 
-(* Coercions *)
+      (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
-          let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+          let s = coerce_global_to_id qid in
+	  VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
-           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+           let s = coerce_global_to_id qid in
+	  VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Local, f, s, t)
@@ -406,114 +426,230 @@ GEXTEND Gram
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
-      | IDENT "Class"; IDENT "Local"; c = global ->
-	  Pp.warning "Class is obsolete"; VernacNop
-      | IDENT "Class"; c = global ->
-	  Pp.warning "Class is obsolete"; VernacNop
 
-(* Implicit *)
-(*
-      | IDENT "Syntactic"; "Definition"; id = identref; ":="; c = constr;
-         n = OPT [ "|"; n = natural -> n ] ->
-	   VernacSyntacticDefinition (id,c,n)
-*)
-      | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr;
-         n = OPT [ "|"; n = natural -> n ] ->
-	   let c = match n with
-	     | Some n ->
-		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
-		 CApp (loc,(None,c),l)
-	     | None -> c in
-	   VernacSyntacticDefinition (id,c,false,true)
-      | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
-	  let l = List.map (fun n -> ExplByPos n) l in
-	  VernacDeclareImplicits (qid,Some l)
-      | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
-
-      | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
-	   idl = LIST1 identref SEP ","; ":"; c = constr -> VernacReserve (idl,c)
-
-      (* For compatibility *)
-      | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
-	  VernacSetOption
-	    (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue true)
-      | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" ->
-	  VernacSetOption
-	    (Goptions.SecondaryTable ("Implicit","Arguments"), BoolValue false)
-  ] ]
+      (* Implicit *)
+      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
+         pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
+	   let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+	   VernacDeclareImplicits (qid,pos)
+
+      | IDENT "Implicit"; ["Type" | IDENT "Types"];
+	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
 END
 
-(* Modules management *)   
-if !Options.v7 then
 GEXTEND Gram
-  GLOBAL: command;
+  GLOBAL: command check_command class_rawexpr;
 
-  export_token:
-    [ [ IDENT "Import" -> false
-      | IDENT "Export" -> true
-      |  -> false ] ]
-  ;
-  specif_token:
-    [ [ IDENT "Implementation" -> Some false
-      | IDENT "Specification" -> Some true
-      |  -> None ] ]
-  ;
   command:
-    [ [ "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
-	s = [ s = STRING -> s | s = IDENT -> s ] ->
+    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
+
+      (* System directory *)
+      | IDENT "Pwd" -> VernacChdir None
+      | IDENT "Cd" -> VernacChdir None
+      | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir)
+
+      (* Toplevel control *)
+      | IDENT "Drop" -> VernacToplevelControl Drop
+      | IDENT "ProtectedLoop" -> VernacToplevelControl ProtectedLoop
+      | IDENT "Quit" -> VernacToplevelControl Quit
+
+      | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
+	s = [ s = ne_string -> s | s = IDENT -> s ] ->
 	  VernacLoad (verbosely, s)
-(*      | "Compile";
-	verbosely =
-          [ IDENT "Verbose" -> "Verbose"
-          | -> "" ];
-	IDENT "Module";
-	only_spec =
-          [ IDENT "Specification" -> "Specification"
-          | -> "" ];
-	mname = [ s = STRING -> s | s = IDENT -> s ];
-	fname = OPT [ s = STRING -> s | s = IDENT -> s ] -> ExtraVernac
-          let fname = match fname with Some s -> s | None -> mname in
-            <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
-                      ($STR $mname) ($STR $fname))>>
-*)
-      | IDENT "Read"; IDENT "Module"; qidl = LIST1 global ->
-	  VernacRequire (None, None, qidl)
-      | IDENT "Require"; export = export_token; specif = specif_token;
-        qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
-(*      | IDENT "Require"; export = export_token; specif = specif_token;
-        id = identref; filename = STRING -> 
-	  VernacRequireFrom (export, specif, id, filename) *)
-      | IDENT "Require"; export = export_token; specif = specif_token;
-        filename = STRING -> 
-	  VernacRequireFrom (Some export, specif, filename)
-      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
+      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
 	  VernacDeclareMLModule l
-      | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
-      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-  ] 
-]
+
+      (* Dump of the universe graph - to file or to stdout *) 
+      | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
+	  VernacPrint (PrintUniverses fopt)
+
+      | IDENT "Locate"; l = locatable -> VernacLocate l
+
+      (* Managing load paths *)
+      | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath ->
+	  VernacAddLoadPath (false, dir, alias)
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; 
+	  alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
+      | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
+	  VernacRemoveLoadPath dir
+
+       (* For compatibility *)
+      | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath ->
+	  VernacAddLoadPath (false, dir, alias)
+      | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath ->
+	  VernacAddLoadPath (true, dir, alias)
+      | IDENT "DelPath"; dir = ne_string ->
+	  VernacRemoveLoadPath dir
+
+      (* Type-Checking (pas dans le refman) *)
+      | "Type"; c = lconstr -> VernacGlobalCheck c
+
+      (* Printing (careful factorization of entries) *)
+      | IDENT "Print"; p = printable -> VernacPrint p
+      | IDENT "Print"; qid = global -> VernacPrint (PrintName qid)
+      | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> 
+	  VernacPrint (PrintModuleType qid)
+      | IDENT "Print"; IDENT "Module"; qid = global -> 
+	  VernacPrint (PrintModule qid)
+      | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
+      | IDENT "About"; qid = global -> VernacPrint (PrintAbout qid)
+
+      (* Searching the environment *)
+      | IDENT "Search"; qid = global; l = in_or_out_modules -> 
+	  VernacSearch (SearchHead qid, l)
+      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
+	  VernacSearch (SearchPattern c, l)
+      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
+	  VernacSearch (SearchRewrite c, l)
+      | IDENT "SearchAbout"; 
+	  sl = [ "["; l = LIST1 [ r = global -> SearchRef r
+                                | s = ne_string -> SearchString s ]; "]" -> l 
+   		 | qid = global -> [SearchRef qid] ];
+	  l = in_or_out_modules -> 
+	  VernacSearch (SearchAbout sl, l)
+
+      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
+	  VernacAddMLPath (false, dir)
+      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
+	  VernacAddMLPath (true, dir)
+
+      (* Pour intervenir sur les tables de param�ètres *)
+      | "Set"; table = IDENT; field = IDENT; v = option_value ->
+  	  VernacSetOption (SecondaryTable (table,field),v)
+      | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
+  	  VernacAddOption (SecondaryTable (table,field),lv)
+      | "Set"; table = IDENT; field = IDENT ->
+  	  VernacSetOption (SecondaryTable (table,field),BoolValue true)
+      | IDENT "Unset"; table = IDENT; field = IDENT ->
+  	  VernacUnsetOption (SecondaryTable (table,field))
+      | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value ->
+  	  VernacRemoveOption (SecondaryTable (table,field),lv)
+      | "Set"; table = IDENT; value = option_value ->
+  	  VernacSetOption (PrimaryTable table, value)
+      | "Set"; table = IDENT ->
+  	  VernacSetOption (PrimaryTable table, BoolValue true)
+      | IDENT "Unset"; table = IDENT ->
+  	  VernacUnsetOption (PrimaryTable table)
+
+      | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT ->
+	  VernacPrintOption (SecondaryTable (table,field))
+      | IDENT "Print"; IDENT "Table"; table = IDENT ->
+	  VernacPrintOption (PrimaryTable table)
+
+      | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
+        -> VernacAddOption (SecondaryTable (table,field), v)
+
+      (* Un value global ci-dessous va �être cach�é par un field au dessus! *)
+      | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
+          VernacAddOption (PrimaryTable table, v)
+
+      | IDENT "Test"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
+        -> VernacMemOption (SecondaryTable (table,field), v)
+      | IDENT "Test"; table = IDENT; field = IDENT ->
+          VernacPrintOption (SecondaryTable (table,field))
+      | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value ->
+          VernacMemOption (PrimaryTable table, v)
+      | IDENT "Test"; table = IDENT ->
+          VernacPrintOption (PrimaryTable table)
+
+      | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
+        -> VernacRemoveOption (SecondaryTable (table,field), v)
+      | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
+	  VernacRemoveOption (PrimaryTable table, v) ] ]
   ;
-END
+  check_command: (* TODO: rapprocher Eval et Check *)
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
+          fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Check"; c = lconstr ->
+	  fun g -> VernacCheckMayEval (None, g, c) ] ]
+  ;
+  printable:
+    [ [ IDENT "Term"; qid = global -> PrintName qid
+      | IDENT "All" -> PrintFullContext
+      | IDENT "Section"; s = global -> PrintSectionContext s
+      | IDENT "Grammar"; ent = IDENT ->
+          (* This should be in "syntax" section but is here for factorization*)
+	  PrintGrammar ("", ent)
+      | IDENT "LoadPath" -> PrintLoadPath
+      | IDENT "Modules" -> PrintModules
 
-if !Options.v7 then
-GEXTEND Gram
-  GLOBAL: command;
+      | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath
+      | IDENT "ML"; IDENT "Modules" -> PrintMLModules
+      | IDENT "Graph" -> PrintGraph
+      | IDENT "Classes" ->  PrintClasses
+      | IDENT "Ltac"; qid = global -> PrintLtac qid
+      | IDENT "Coercions" -> PrintCoercions
+      | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
+         -> PrintCoercionPaths (s,t)
+      | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
+      | IDENT "Tables" -> PrintTables
+(* Obsolete: was used for cooking V6.3 recipes ??
+      | IDENT "Proof"; qid = global -> PrintOpaqueName qid
+*)
+      | IDENT "Hint" -> PrintHintGoal
+      | IDENT "Hint"; qid = global -> PrintHint qid
+      | IDENT "Hint"; "*" -> PrintHintDb
+      | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
+      | IDENT "Setoids" -> PrintSetoids
+      | IDENT "Scopes" -> PrintScopes
+      | IDENT "Scope"; s = IDENT -> PrintScope s
+      | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
+  ;
+  class_rawexpr:
+    [ [ IDENT "Funclass" -> FunClass
+      | IDENT "Sortclass" -> SortClass
+      | qid = global -> RefClass qid ] ]
+  ;
+  locatable:
+    [ [ qid = global -> LocateTerm qid
+      | IDENT "File"; f = ne_string -> LocateFile f
+      | IDENT "Library"; qid = global -> LocateLibrary qid
+      | IDENT "Module"; qid = global -> LocateModule qid
+      | s = ne_string -> LocateNotation s ] ]
+  ;
+  option_value:
+    [ [ n  = integer   -> IntValue n
+      | s  = STRING    -> StringValue s ] ]
+  ;
+  option_ref_value:
+    [ [ id = global   -> QualidRefValue id
+      | s  = STRING   -> StringRefValue s ] ]
+  ;
+  as_dirpath:
+    [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
+  ;
+  in_or_out_modules:
+    [ [ IDENT "inside"; l = LIST1 global -> SearchInside l
+      | IDENT "outside"; l = LIST1 global -> SearchOutside l
+      | -> SearchOutside [] ] ]
+  ;
+  comment:
+    [ [ c = constr -> CommentConstr c
+      | s = STRING -> CommentString s
+      | n = natural -> CommentInt n ] ]
+  ;
+END;
 
+GEXTEND Gram
   command:
     [ [ 
-
 (* State management *)
         IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s
-      | IDENT "Write"; IDENT "State"; s = STRING -> VernacWriteState s
+      | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s
       | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s
-      | IDENT "Restore"; IDENT "State"; s = STRING -> VernacRestoreState s
+      | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s
 
 (* Resetting *)
       | IDENT "Reset"; id = identref -> VernacResetName id
       | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
+      | IDENT "BackTo"; n = natural -> VernacBackTo n
+      | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> 
+	  VernacBacktrack (n,m,p)
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" -> VernacDebug true
@@ -522,3 +658,86 @@ GEXTEND Gram
  ] ];
     END
 ;;
+
+(* Grammar extensions *)
+	  
+GEXTEND Gram
+  GLOBAL: syntax;
+
+  syntax:
+   [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
+         VernacOpenCloseScope (local,true,sc)
+
+     | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> 
+         VernacOpenCloseScope (local,false,sc)
+
+     | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
+	 VernacDelimiters (sc,key)
+
+     | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; 
+       refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
+
+     | IDENT "Arguments"; IDENT "Scope"; qid = global;
+         "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
+
+     | IDENT "Infix"; local = locality;
+	 op = ne_string; ":="; p = global; 
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
+         VernacInfix (local,(op,modl),p,sc)
+     | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
+	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
+           VernacSyntacticDefinition (id,c,local,b)
+     | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
+           VernacNotation (local,c,(s,modl),sc)
+
+     | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
+	 pil = LIST1 production_item; ":="; t = Tactic.tactic
+         -> VernacTacticNotation (n,pil,t)
+
+     | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
+	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
+	 -> VernacSyntaxExtension (local,(s,l))
+
+     (* "Print" "Grammar" should be here but is in "command" entry in order 
+        to factorize with other "Print"-based vernac entries *)
+  ] ]
+  ;
+  tactic_level:
+    [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ]
+  ;
+  locality:
+    [ [ IDENT "Local" -> true | -> false ] ]
+  ;
+  level:
+    [ [ IDENT "level"; n = natural -> NumLevel n
+      | IDENT "next"; IDENT "level" -> NextLevel ] ]
+  ;
+  syntax_modifier:
+    [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; 
+        lev = level -> SetItemLevel (x::l,lev)
+      | "at"; IDENT "level"; n = natural -> SetLevel n
+      | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
+      | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
+      | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
+      | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
+      | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
+  ;
+  syntax_extension_type:
+    [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
+      | IDENT "bigint" -> ETBigint
+    ] ]
+  ;
+  opt_scope:
+    [ [ "_" -> None | sc = IDENT -> Some sc ] ]
+  ;
+  production_item:
+    [ [ s = ne_string -> VTerm s
+      | nt = IDENT; po = OPT [ "("; p = ident; ")" -> p ] -> 
+	  VNonTerm (loc,nt,po) ] ]
+  ;
+END