*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7

39 files changed, 2970 insertions, 356 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 576c57a53..4d6edda0e 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -78,7 +78,7 @@ let make_rule loc (prods,act) =
   let (symbs,pil) = List.split prods in
   <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >>
 
-let declare_tactic_argument loc s typ pr f rawtyppr cl =
+let declare_tactic_argument for_v8 loc s typ pr f rawtyppr cl =
   let interp = match f with
     | None -> <:expr< Tacinterp.genarg_interp >>
     | Some f -> <:expr< $lid:f$>> in
@@ -103,12 +103,13 @@ let declare_tactic_argument loc s typ pr f rawtyppr cl =
       Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
         [(None, None, $rules$)];
       Pptactic.declare_extra_genarg_pprule
+        $mlexpr_of_bool for_v8$
         ($rawwit$, $lid:rawpr$)
         ($wit$, $lid:pr$);
     end
   >>
 
-let declare_vernac_argument loc s cl =
+let declare_vernac_argument for_v8 loc s cl =
   let se = mlexpr_of_string s in
   let typ = ExtraArgType s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
@@ -173,13 +174,31 @@ EXTEND
         "END" ->
 	  if String.capitalize s = s then
 	    failwith "Argument entry names must be lowercase";
-         declare_tactic_argument loc s typ pr f rawtyppr l
+         declare_tactic_argument true loc s typ pr f rawtyppr l
       | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
         OPT "|"; l = LIST1 argrule SEP "|";
         "END" ->
 	  if String.capitalize s = s then
 	    failwith "Argument entry names must be lowercase";
-         declare_vernac_argument loc s l ] ]
+         declare_vernac_argument true loc s l
+      | "V7"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        "TYPED"; "AS"; typ = argtype;
+        "PRINTED"; "BY"; pr = LIDENT;
+        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
+        rawtyppr =
+          OPT [ "RAW"; "TYPED"; "AS"; t = argtype; 
+                "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
+        OPT "|"; l = LIST1 argrule SEP "|";
+        "END" ->
+	  if String.capitalize s = s then
+	    failwith "Argument entry names must be lowercase";
+         declare_tactic_argument false loc s typ pr f rawtyppr l
+      | "V7"; "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        OPT "|"; l = LIST1 argrule SEP "|";
+        "END" ->
+	  if String.capitalize s = s then
+	    failwith "Argument entry names must be lowercase";
+         declare_vernac_argument false loc s l ] ]
   ;
   argtype:
     [ [ e = LIDENT -> fst (interp_entry_name loc e) ] ]
diff --git a/parsing/ast.ml b/parsing/ast.ml
index 13989bcbb..1b68f69bf 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -122,21 +122,35 @@ type grammar_action =
 
 type env = (string * typed_ast) list
 
+let string_of_dirpath = function
+  | [] -> "<empty>"
+  | sl ->
+      String.concat "." (List.map string_of_id (List.rev sl))
+
+let pr_id id = str (string_of_id id)
+
+let print_kn kn =
+  let (mp,dp,l) = repr_kn kn in
+  let dpl = repr_dirpath dp in
+  str (string_of_mp mp) ++ str "." ++
+  prlist_with_sep (fun _ -> str".") pr_id dpl ++
+  str (string_of_label l)
+
 (* Pretty-printing *)
 let rec print_ast ast =
   match ast with
     | Num(_,n) -> int n
     | Str(_,s) -> qs s
-    | Path(_,sl) -> str (string_of_kn sl)
+    | Path(_,sl) -> print_kn sl
     | Id (_,s) -> str "{" ++ str s ++ str "}"
-    | Nvar(_,s) -> str (string_of_id s)
+    | Nvar(_,s) -> pr_id s
     | Nmeta(_,s) -> str s
     | Node(_,op,l) ->
         hov 3 (str "(" ++ str op ++ spc () ++ print_astl l ++ str ")")
     | Slam(_,None,ast) -> hov 1 (str "[<>]" ++ print_ast ast)
     | Slam(_,Some x,ast) ->
         hov 1
-          (str "[" ++ str (string_of_id x) ++ str "]" ++ cut () ++ 
+          (str "[" ++ pr_id x ++ str "]" ++ cut () ++ 
 	   print_ast ast)
     | Smetalam(_,id,ast) -> hov 1 (str id ++ print_ast ast)
     | Dynamic(_,d) ->
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 192f84d6b..77ac447c9 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -42,11 +42,26 @@ let assoc_level = function
   | _ -> ""
 
 let constr_level = function
-  | 8,assoc -> assert (assoc <> Gramext.LeftA); "top"
   | n,assoc -> (string_of_int n)^(assoc_level assoc)
 
-let default_levels = [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA]
-let level_stack = ref [default_levels]
+let default_levels_v7 =
+  [10,Gramext.RightA;
+   9,Gramext.RightA;
+   8,Gramext.RightA;
+   1,Gramext.RightA;
+   0,Gramext.RightA]
+
+let default_levels_v8 =
+  [200,Gramext.RightA;
+   100,Gramext.RightA;
+   80,Gramext.RightA;
+   40,Gramext.LeftA;
+   10,Gramext.LeftA;
+   9,Gramext.RightA;
+   1,Gramext.LeftA;
+   0,Gramext.RightA]
+
+let level_stack = ref [default_levels_v7]
 
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
@@ -65,15 +80,17 @@ let create_assoc = function
   | Some a -> a
 
 let find_position other assoc lev =
+  let default =
+    if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
   let current = List.hd !level_stack in 
   match lev with
   | None ->
       level_stack := current :: !level_stack;
       None, (if other then assoc else None), None
   | Some n ->
-      if n = 8 & assoc = Some Gramext.LeftA then 
+      if !Options.v7 & n = 8 & assoc = Some Gramext.LeftA then 
 	error "Left associativity not allowed at level 8";
-      let after = ref (8,Gramext.RightA) in
+      let after = ref default in
       let rec add_level q = function
         | (p,_ as pa)::l when p > n -> pa :: add_level pa l
         | (p,a as pa)::l as l' when p = n ->
@@ -92,7 +109,7 @@ let find_position other assoc lev =
       try
 	(* Create the entry *)
         let current = List.hd !level_stack in
-        level_stack := add_level (8,Gramext.RightA) current :: !level_stack;
+        level_stack := add_level default current :: !level_stack;
 	let assoc = create_assoc assoc in
         Some (Gramext.After (constr_level !after)),
 	Some assoc, Some (constr_level (n,assoc))
@@ -347,7 +364,7 @@ let extend_constr_notation (n,assoc,ntn,rule) =
 
 let extend_constr_delimiters (sc,rule,pat_rule) =
   let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.constr (ETConstr(0,()),Some 0,Some Gramext.NonA,false)
+  extend_constr Constr.operconstr (ETConstr(0,()),Some 0,Some Gramext.NonA,false)
     (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
   extend_constr Constr.pattern (ETPattern,None,None,false)
@@ -361,13 +378,21 @@ let make_rule univ f g (s,pt) =
   let act = make_gen_act f ntl in
   (symbs, act)
 
+let tac_exts = ref []
+let get_extend_tactic_grammars () = !tac_exts
+
 let extend_tactic_grammar s gl =
+  tac_exts := (s,gl) :: !tac_exts;
   let univ = get_univ "tactic" in
   let make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
   let rules = List.map (make_rule univ make_act make_prod_item) gl in
   Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
 
+let vernac_exts = ref []
+let get_extend_vernac_grammars () = !vernac_exts
+
 let extend_vernac_command_grammar s gl =
+  vernac_exts := (s,gl) :: !vernac_exts;
   let univ = get_univ "vernac" in
   let make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in
   let rules = List.map (make_rule univ make_act make_prod_item) gl in
@@ -418,6 +443,15 @@ let extend_grammar gram =
   | TacticGrammar l -> add_tactic_entries l);
   grammar_state := gram :: !grammar_state
 
+let reset_extend_grammars_v8 () =
+  let te = List.rev !tac_exts in
+  let tv = List.rev !vernac_exts in
+  tac_exts := [];
+  vernac_exts := [];
+  List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
+  List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv;
+  level_stack := [default_levels_v8]
+
 
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
@@ -448,12 +482,10 @@ let unfreeze (grams, lex) =
   grammar_state := common;
   Lexer.unfreeze lex;
   List.iter extend_grammar (List.rev redo)
-    
+ 
 let init_grammar () =
   remove_grammars (number_of_entries !grammar_state);
   grammar_state := []
 
-let _ = Lexer.init ()
-
 let init () =
   init_grammar ()
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index d24264abc..091f98424 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -42,5 +42,11 @@ val extend_tactic_grammar :
 val extend_vernac_command_grammar :
   string -> (string * grammar_tactic_production list) list -> unit
 
+val get_extend_tactic_grammars :
+ unit -> (string * (string * grammar_tactic_production list) list) list
+val get_extend_vernac_grammars :
+ unit -> (string * (string * grammar_tactic_production list) list) list
+val reset_extend_grammars_v8 : unit -> unit
+
 val subst_all_grammar_command :
   Names.substitution -> all_grammar_command -> all_grammar_command
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 14a33a656..076f7f026 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -175,7 +175,8 @@ let explicitize_prod_entry pos univ nt =
   | "constr5" -> ETConstr (5,pos)
   | "constr6" -> ETConstr (6,pos)
   | "constr7" -> ETConstr (7,pos)
-  | "constr8" | "constr" -> ETConstr (8,pos)
+  | "constr8" -> ETConstr (8,pos)
+  | "constr" when !Options.v7 -> ETConstr (8,pos)
   | "constr9" -> ETConstr (9,pos)
   | "constr10" | "lconstr" -> ETConstr (10,pos)
   | "pattern" -> ETPattern
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 683b2ae54..a1208f48c 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -18,6 +18,15 @@ open Goptions
 open Constr
 open Prim
 
+let vernac_kw =
+  [ "Quit"; "Load"; "Compile"; "Fixpoint"; "CoFixpoint";
+    "Definition"; "Inductive"; "CoInductive"; 
+    "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
+    "."; ">->" ]
+let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
+
+let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
+
 GEXTEND Gram
   GLOBAL: class_rawexpr;
 
@@ -155,7 +164,7 @@ GEXTEND Gram
     [ [ IDENT "Term"; qid = global -> PrintName qid
       | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
-      | "Grammar"; uni = IDENT; ent = IDENT ->
+      | IDENT "Grammar"; uni = IDENT; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
 	  PrintGrammar (uni, ent)
       | IDENT "LoadPath" -> PrintLoadPath
@@ -213,19 +222,19 @@ GEXTEND Gram
    [ [ IDENT "Token"; s = STRING ->
        Pp.warning "Token declarations are now useless"; VernacNop
 
-     | "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
+     | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
         OPT [ ":"; IDENT "tactic" ]; ":=";
         OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> 
 	  VernacTacticGrammar tl
 
-     | "Grammar"; u = univ;
+     | IDENT "Grammar"; u = univ;
          tl = LIST1 grammar_entry SEP "with" -> 
 	   VernacGrammar (rename_command_entry u,tl)
 
-     | "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
+     | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
-     | "Uninterpreted"; IDENT "Notation"; s = STRING; 
+     | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
 	 -> VernacSyntaxExtension (s,l)
 
@@ -237,19 +246,46 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
-     | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING; 
+     | IDENT "Infix"; a = entry_prec; n = OPT natural;
+         op = STRING; 
          p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in
-         VernacInfix (a,n,op,p,b,sc)
+	 sc = OPT [ ":"; sc = IDENT -> sc];
+         v8 = OPT[IDENT "V8only";
+                  op8=OPT STRING;
+                  n8=OPT natural;
+                  mv8=OPT["("; l = LIST1 syntax_modifier SEP ","; ")" -> l] ->
+                    (op8,n8,mv8) ] ->
+           let (ai,ni,b) = Metasyntax.interp_infix_modifiers a n modl in
+           let v8 =
+             let (op8,nv8,mv8) =
+               match v8 with
+                   Some (op8,nv8,mv8) ->
+                     let op8 = match op8 with Some s -> s | _ -> op in
+                     let nv8 = match nv8 with Some n -> Some n
+                       | _ -> Util.option_app (( * ) 10) n in
+                     let mv8 = match mv8 with Some m -> m | _ -> modl in
+                     (op8,nv8,mv8)
+                 | None ->  (op,Util.option_app(( * ) 10) n, modl) in
+             let (a8,n8,_) =
+               Metasyntax.interp_infix_modifiers a nv8 mv8 in
+             Some(a8,n8,op8) in
+           VernacInfix (ai,ni,op,p,b,v8,sc)
      | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
 	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
      | IDENT "Notation"; s = IDENT; ":="; c = constr ->
-	 VernacNotation ("'"^s^"'",c,[],None)
+	 VernacNotation ("'"^s^"'",c,[],None,None)
      | IDENT "Notation"; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
-	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (s,c,modl,sc)
+	 sc = OPT [ ":"; sc = IDENT -> sc ];
+         v8 = OPT[IDENT "V8only";
+                  s8=OPT STRING;
+                  mv8=["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8
+                      | ->[] ] -> (s8,mv8) ] ->
+           let v8 = Util.option_app (fun (s8,mv8) ->
+             let s8 = match s8 with Some s -> s | _ -> s in
+             (s8,mv8)) v8 in
+           VernacNotation (s,c,modl,v8,sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
@@ -269,9 +305,8 @@ GEXTEND Gram
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
-      | IDENT "annot" ->
-	  if !Options.v7 <> true then Util.error "annot not allowed in new syntax";
-	  ETOther ("constr","annot")
+      | IDENT "bigint" -> ETBigint
+      | i=IDENT -> ETOther ("constr",i)
     ] ]
   ;
   opt_scope:
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 62ee20cad..679d174c2 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -20,7 +20,7 @@ let pair loc =
   Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair")
 
 GEXTEND Gram
-  GLOBAL: constr pattern;
+  GLOBAL: operconstr pattern;
 
   pattern:
     [ [ r = Prim.reference -> CPatAtom (loc,Some r)
@@ -47,12 +47,12 @@ GEXTEND Gram
       | p = pattern -> p ] ]
   ;
   equation:
-    [ [ lhs = LIST1 pattern; "=>"; rhs = constr9 -> (loc,lhs,rhs) ] ]
+    [ [ lhs = LIST1 pattern; "=>"; rhs = operconstr LEVEL "9" -> (loc,lhs,rhs) ] ]
   ;
   ne_eqn_list:
     [ [ leqn = LIST1 equation SEP "|" -> leqn ] ]
   ;
-  constr: LEVEL "1"
+  operconstr: LEVEL "1"
     [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
 	  CCases (loc, Some p, lc, eqs)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index eac6ce12f..cea564953 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,6 +17,19 @@ open Libnames
 open Prim
 open Topconstr
 
+(* Initialize the lexer *)
+let constr_kw =
+  [ "Cases"; "of"; "with"; "end"; "as"; "in"; "Prop"; "Set"; "Type";
+    ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!";
+    "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/";
+    "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-";
+    "~"; "'"; "<<"; ">>"; "<>";
+  ]
+let _ = List.iter (fun s -> Lexer.add_token ("",s)) constr_kw
+(* "let" is not a keyword because #Core#let.cci would not parse.
+   Is it still accurate ? *)
+
+
 let coerce_to_var = function
   | CRef (Ident (_,id)) -> id
   | ast -> Util.user_err_loc
@@ -78,8 +91,9 @@ let test_ident_colon =
             end
         | _ -> raise Stream.Failure)
 
+
 GEXTEND Gram
-  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident annot
+  GLOBAL: operconstr lconstr constr sort global constr_pattern Constr.ident annot
           (*ne_name_comma_list*);
   Constr.ident:
     [ [ id = Prim.ident -> id
@@ -105,8 +119,24 @@ GEXTEND Gram
       | "Type" -> RType None ] ]
   ;
   constr:
-    [ "top" RIGHTA
-      [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
+    [ [ c = operconstr LEVEL "8" -> c ] ]
+  ;
+  lconstr:
+    [ [ c = operconstr LEVEL "10" -> c ] ]
+  ;
+  operconstr:
+    [ "10" RIGHTA
+      [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") ->
+          CAppExpl (loc, f, args)
+(*
+      | "!"; f = global; "with"; b = binding_list ->
+	  <:ast< (APPLISTWITH $f $b) >>
+*)
+      | f = operconstr; args = LIST1 constr91 -> CApp (loc, f, args) ]
+    | "9" RIGHTA
+      [ c1 = operconstr; "::"; c2 = operconstr -> CCast (loc, c1, c2) ]
+    | "8" RIGHTA
+      [ c1 = operconstr; "->"; c2 = operconstr -> CArrow (loc, c1, c2) ]
     | "1" RIGHTA
       [ "<"; p = annot; ">"; IDENT "Match"; c = constr; "with";
         cl = LIST0 constr; "end" ->
@@ -119,32 +149,32 @@ GEXTEND Gram
       | IDENT "Match"; c = constr; "with"; cl = LIST1 constr; "end" ->
           COrderedCase (loc, MatchStyle, None, c, cl)
       | IDENT "let"; "("; b = ne_name_comma_list; ")"; "=";
-        c = constr; "in"; c1 = constr LEVEL "top"->
+        c = constr; "in"; c1 = constr ->
           (* TODO: right loc *)
 	  COrderedCase
             (loc, LetStyle, None, c, [CLambdaN (loc, [b, CHole loc], c1)])
       | IDENT "let"; na = name; "="; c = opt_casted_constr; 
-	"in"; c1 = constr LEVEL "top" ->
+	"in"; c1 = constr ->
           CLetIn (loc, na, c, c1)
       | IDENT "if"; c1 = constr;
         IDENT "then"; c2 = constr;
-        IDENT "else"; c3 = constr LEVEL "top" ->
+        IDENT "else"; c3 = constr ->
 	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
       | "<"; p = annot; ">";
         IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; 
-        "in"; c1 = constr LEVEL "top" ->
+        "in"; c1 = constr ->
           (* TODO: right loc *)
 	  COrderedCase (loc, LetStyle, Some p, c,
             [CLambdaN (loc, [b, CHole loc], c1)])
       | "<"; p = annot; ">";
         IDENT "if"; c1 = constr;
         IDENT "then"; c2 = constr; 
-        IDENT "else"; c3 = constr LEVEL "top" ->
+        IDENT "else"; c3 = constr ->
 	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
     | "0" RIGHTA
       [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CMeta (loc, n)
-      | bll = binders; c = constr LEVEL "top" -> abstract_constr loc c bll
+      | bll = binders; c = constr -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
       | "("; test_int_rparen; n = bigint; ")" ->
           CDelimiters (loc,"N",CNumeral (loc,n))
@@ -182,24 +212,10 @@ GEXTEND Gram
       | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
           CDelimiters (loc,key,c) ] ]
   ;
-  lconstr:
-    [ "10" RIGHTA
-      [ "!"; f = global; args = LIST0 constr9 -> CAppExpl (loc, f, args)
-(*
-      | "!"; f = global; "with"; b = binding_list ->
-	  <:ast< (APPLISTWITH $f $b) >>
-*)
-      | f = constr9; args = LIST1 constr91 -> CApp (loc, f, args)
-      | f = constr9 -> f ] ]
-  ;
   constr91:
-    [ [ test_int_bang; n = INT; "!"; c = constr9 ->
+    [ [ test_int_bang; n = INT; "!"; c = operconstr LEVEL "9" ->
         (c, Some (int_of_string n))
-      | c = constr9 -> (c, None) ] ]
-  ;
-  constr9:
-    [ RIGHTA [ c1 = constr -> c1
-      | c1 = constr; "::"; c2 = constr -> CCast (loc, c1, c2) ] ]
+      | c = operconstr LEVEL "9" -> (c, None) ] ]
   ;
   (* annot and product_annot_tail are hacks to forbid concrete syntax *)
   (* ">" (e.g. for gt, Zgt, ...) in annotations *)
@@ -232,7 +248,7 @@ GEXTEND Gram
       [ c1 = SELF; "=="; c2 = NEXT -> CNotation (loc, "_ == _", [c1;c2]) ]
     | RIGHTA
       [ c1 = SELF; "="; c2 = NEXT -> CNotation (loc, "_ = _", [c1;c2]) ]
-    | [ c = constr LEVEL "4L" -> c ] ]
+    | [ c = operconstr LEVEL "4L" -> c ] ]
   ;
   product_annot_tail:
     [ [ ";"; idl = ne_name_comma_list; ":"; c = constr;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
new file mode 100644
index 000000000..ba8be907c
--- /dev/null
+++ b/parsing/g_constrnew.ml4
@@ -0,0 +1,256 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pcoq
+open Constr
+open Prim
+open Rawterm
+open Term
+open Names
+open Libnames
+open Topconstr
+
+open Util
+
+let constr_kw =
+  [ "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as";
+    "let"; "if"; "then"; "else"; "struct"; "Prop"; "Set"; "Type" ]
+let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
+let _ = Options.v7 := false
+
+let pair loc =
+  Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair")
+
+let mk_cast = function
+    (c,(_,None)) -> c
+  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, ty)
+
+let mk_lam = function
+    ([],c) -> c
+  | (bl,c) -> CLambdaN(constr_loc c, bl,c)
+
+let coerce_to_id c =
+  match c with
+      CRef(Ident(loc,id)) -> (loc,Name id)
+    | CHole loc -> (loc,Anonymous)
+    | _ -> error "ill-formed match type annotation"
+
+let match_bind_of_pat loc (oid,ty) =
+  let l2 =
+    match oid with
+        None -> []
+      | Some x -> [([x],CHole loc)] in
+  let l1 =
+    match ty with
+        None -> [] (* No: should lookup inductive arity! *)
+      | Some (CApp(_,_,args)) -> (* parameters do not appear *)
+          List.map (fun (c,_) -> ([coerce_to_id c],CHole loc)) args
+      | _ -> error "ill-formed match type annotation" in
+  l1@l2
+
+let mk_match (loc,cil,rty,br) =
+  let (lc,pargs) = List.split cil in
+  let pr =
+    match rty with
+        None -> None
+      | Some ty ->
+          let idargs = (* TODO: not forget the list lengths for PP! *)
+            List.flatten (List.map (match_bind_of_pat loc) pargs) in
+          Some (CLambdaN(loc,idargs,ty)) in
+  CCases(loc,pr,lc,br)
+
+let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
+  let n =
+    match bl,ann with
+        [([_],_)], None -> 0
+      | _, Some x ->
+          let ids = List.map snd (List.flatten (List.map fst bl)) in
+          (try list_index (snd x) ids - 1
+          with Not_found -> error "no such fix variable")
+      | _ -> error "cannot find decreasing arg of fix" in
+  let ty = match tyc with
+      None -> CHole tloc
+    | Some t -> CProdN(loc,bl,t) in
+  (snd id,n,ty,CLambdaN(loc,bl,body))
+
+let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
+  let _ = option_app (fun (aloc,_) ->
+    Util.user_err_loc
+      (aloc,"Constr:mk_cofixb",
+       Pp.str"Annotation forbidden in cofix expression")) ann in
+  let ty = match tyc with
+      None -> CHole tloc
+    | Some t -> CProdN(loc,bl,t) in
+  (snd id,ty,CLambdaN(loc,bl,body))
+
+let mk_fix(loc,kw,id,dcls) =
+  if kw then 
+    let fb = List.map mk_fixb dcls in
+    CFix(loc,id,fb)
+  else
+    let fb = List.map mk_cofixb dcls in
+    CCoFix(loc,id,fb)
+
+let binder_constr =
+  create_constr_entry (get_univ "constr") "binder_constr"
+
+GEXTEND Gram
+  GLOBAL: binder_constr lconstr constr operconstr sort global
+  constr_pattern Constr.ident;
+  Constr.ident:
+    [ [ id = Prim.ident -> id
+
+      (* This is used in quotations and Syntax *)
+      | id = METAIDENT -> id_of_string id ] ]
+  ;
+  global:
+    [ [ r = Prim.reference -> r
+
+      (* This is used in quotations *)
+      | id = METAIDENT -> Ident (loc,id_of_string id) ] ]
+  ;
+  constr_pattern:
+    [ [ c = constr -> c ] ]
+  ;
+  sort:
+    [ [ "Set"  -> RProp Pos
+      | "Prop" -> RProp Null
+      | "Type" -> RType None ] ]
+  ;
+  lconstr:
+    [ [ c = operconstr -> c ] ]
+  ;
+  constr:
+    [ [ c = operconstr LEVEL "9" -> c ] ]
+  ;
+  operconstr:
+    [ "200" RIGHTA
+      [ c = binder_constr -> c ]
+    | "100" RIGHTA
+      [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2)
+      | c1 = operconstr; ":"; c2 = operconstr    -> CCast(loc,c1,c2) ]
+    | "80" RIGHTA
+      [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
+      | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
+    | "40L" LEFTA
+      [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
+    | "10L" LEFTA
+      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,f,args)
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,f,args) ]
+    | "9" [ ]
+    | "1L" LEFTA
+      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
+    | "0"
+      [ c=atomic_constr -> c
+      | c=match_constr -> c
+      | "("; c=operconstr; ")" -> c ] ]
+  ;
+  binder_constr:
+    [ [ "!"; bl = LIST1 binder; "."; c = operconstr LEVEL "200" ->
+          CProdN(loc,bl,c)
+      | "fun"; bl = LIST1 binder; ty = type_cstr; "=>";
+        c = operconstr LEVEL "200" ->
+          CLambdaN(loc,bl,mk_cast(c,ty))
+      | "let"; id=name; bl = LIST0 binder; ty = type_cstr; ":=";
+        c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+          CLetIn(loc,id,mk_lam(bl,mk_cast(c1,ty)),c2)
+      | "let"; "("; lb = LIST1 name SEP ","; ")"; ":=";
+        c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+          COrderedCase (loc, LetStyle, None, c1,
+                        [CLambdaN (loc, [lb, CHole loc], c2)])
+      | "if"; c1=operconstr; "then"; c2=operconstr LEVEL "200";
+        "else"; c3=operconstr LEVEL "200" ->
+          COrderedCase (loc, IfStyle, None, c1, [c2; c3])
+      | c=fix_constr -> c ] ]
+  ;
+  appl_arg:
+    [ [ "@"; n=INT; ":="; c=operconstr LEVEL "9" -> (c,Some(int_of_string n))
+      | c=operconstr LEVEL "9" -> (c,None) ] ]
+  ;
+  atomic_constr:
+    [ [ g=global -> CRef g
+      | s=sort -> CSort(loc,s)
+      | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
+      | IDENT "_" -> CHole loc
+      | "?"; n=Prim.natural -> CMeta(loc,n) ] ]
+  ;
+  fix_constr:
+    [ [ kw=fix_kw; dcl=fix_decl ->
+          let (_,n,_,_,_,_) = dcl in mk_fix(loc,kw,n,[dcl])
+      | kw=fix_kw; dcl1=fix_decl; "with"; dcls=LIST1 fix_decl SEP "with";
+        "for"; id=identref ->
+          mk_fix(loc,kw,id,dcl1::dcls)
+    ] ]
+    ;
+  fix_kw:
+    [ [ "fix" -> true
+      | "cofix" -> false ] ]
+  ;
+  fix_decl:
+    [ [ id=identref; bl=LIST0 binder; ann=fixannot; ty=type_cstr; ":=";
+        c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
+  ;
+  fixannot:
+    [ [ "{"; "struct"; id=name; "}" -> Some id
+      | -> None ] ]
+  ;
+  match_constr:
+    [ [ "match"; ci=LIST1 case_item SEP ","; ty=case_type; "with";
+        br=branches; "end" -> mk_match (loc,ci,ty,br) ] ]
+  ;
+  case_item:
+    [ [ c=operconstr LEVEL "80"; p=pred_pattern -> (c,p) ] ]
+  ;
+  pred_pattern:
+    [ [ oid = OPT ["as"; id=name -> id];
+        (_,ty) = type_cstr -> (oid,ty) ] ]
+  ;
+  case_type:
+    [ [ ty = OPT [ "=>"; c = lconstr -> c ] -> ty ] ]
+  ;
+  branches:
+    [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
+  ;
+  eqn:
+    [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
+  ;
+  simple_pattern:
+    [ [ r = Prim.reference -> CPatAtom (loc,Some r)
+      | IDENT "_" -> CPatAtom (loc,None)
+      | "("; p = lpattern; ")" -> p
+      | n = bigint -> CPatNumeral (loc,n)
+    ] ]
+  ;
+  pattern:
+    [ [ p = pattern ; lp = LIST1 simple_pattern ->
+        (match p with
+          | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
+          | _ -> Util.user_err_loc 
+              (loc, "compound_pattern", Pp.str "Constructor expected"))
+      | p = pattern; "as"; id = base_ident ->
+	  CPatAlias (loc, p, id)
+      | c = pattern; "%"; key=IDENT -> 
+          CPatDelimiters (loc,key,c)
+      | p = simple_pattern -> p ] ]
+  ;
+  lpattern:
+    [ [ c = pattern -> c
+      | p1=pattern; ","; p2=lpattern ->  CPatCstr (loc, pair loc, [p1;p2]) ] ]
+  ;
+  binder:
+    [ [ id=name -> ([id],CHole loc)
+      | "("; id=name; ")" -> ([id],CHole loc)
+      | "("; id=name; ":"; c=lconstr; ")" -> ([id],c)
+      | id=name; ":"; c=constr -> ([id],c) ] ] (* tolerance *)
+  ;
+  type_cstr:
+    [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
+  ;
+END;;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 7d82fa715..1cc0c0297 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -60,6 +60,10 @@ end
 
 open Prelude
 
+let arg_of_expr = function
+    TacArg a -> a
+  | e -> Tacexp e
+    
 (* Tactics grammar rules *)
 
 GEXTEND Gram
@@ -220,8 +224,8 @@ GEXTEND Gram
       | ta = tactic_arg0 -> ta ] ]
   ;
   tactic_arg0:
-    [ [ "("; a = tactic_expr; ")" -> Tacexp a
-      | "()" -> TacVoid
+    [ [ "("; a = tactic_expr; ")" -> arg_of_expr a
+      | "()" -> Integer 0
       | r = reference -> Reference r
       | n = integer -> Integer n
       | id = METAIDENT -> MetaIdArg (loc,id)
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
new file mode 100644
index 000000000..fe7c17ad1
--- /dev/null
+++ b/parsing/g_ltacnew.ml4
@@ -0,0 +1,209 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Ast
+open Topconstr
+open Rawterm
+open Tacexpr
+open Vernacexpr
+open Ast
+
+ifdef Quotify then
+open Qast
+else
+open Pcoq
+
+open Prim
+open Tactic
+
+ifdef Quotify then
+open Q
+
+type let_clause_kind =
+  | LETTOPCLAUSE of Names.identifier * constr_expr
+  | LETCLAUSE of
+      (Names.identifier Util.located * constr_expr may_eval option * raw_tactic_arg)
+
+ifdef Quotify then
+module Prelude = struct
+let fail_default_value = Qast.Int "0"
+
+let out_letin_clause loc = function
+  | Qast.Node ("LETTOPCLAUSE", _) -> user_err_loc (loc, "", (str "Syntax Error"))
+  | Qast.Node ("LETCLAUSE", [id;c;d]) ->
+      Qast.Tuple [id;c;d]
+  | _ -> anomaly "out_letin_clause"
+
+let make_letin_clause _ = function
+  | Qast.List l -> Qast.List (List.map (out_letin_clause dummy_loc) l)
+  | _ -> anomaly "make_letin_clause"
+end
+else
+module Prelude = struct
+let fail_default_value = 0
+
+let out_letin_clause loc = function
+  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
+  | LETCLAUSE (id,c,d) -> (id,c,d)
+
+let make_letin_clause loc = List.map (out_letin_clause loc)
+end
+
+let arg_of_expr = function
+    TacArg a -> a
+  | e -> Tacexp e
+    
+open Prelude
+
+(* Tactics grammar rules *)
+
+let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
+
+GEXTEND Gram
+  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg;
+
+  tactic_expr:
+    [ "5" LEFTA
+      [ ta0 = tactic_expr; "&"; ta1 = tactic_expr -> TacThen (ta0, ta1)
+      | ta = tactic_expr; "&"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
+          TacThens (ta, lta) ]
+    | "4"
+      [ ]
+    | "3" RIGHTA
+      [ IDENT "try"; ta = tactic_expr -> TacTry ta
+      | IDENT "do"; n = natural; ta = tactic_expr -> TacDo (n,ta)
+      | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
+      | IDENT "progress"; ta = tactic_expr -> TacProgress ta
+      | IDENT "info"; tc = tactic_expr -> TacInfo tc ]
+    | "2" RIGHTA
+      [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
+    | "1" RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
+          TacFun (it,body)
+      | IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+          body = tactic_expr -> TacLetRecIn (rcl,body)
+      | "let"; llc = LIST1 let_clause SEP "with"; "in";
+          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
+      | "match"; IDENT "context"; "with"; mrl = match_context_list; "end" ->
+          TacMatchContext (false,mrl)
+      | "match"; IDENT "reverse"; IDENT "context"; "with";
+        mrl = match_context_list; "end" ->
+          TacMatchContext (true,mrl)
+      |	"match"; c = constrarg; "with"; mrl = match_list; "end" ->
+          TacMatch (c,mrl)
+(*To do: put Abstract in Refiner*)
+      | IDENT "abstract"; tc = tactic_expr -> TacAbstract (tc,None)
+      | IDENT "abstract"; tc = tactic_expr; "using";  s = base_ident ->
+          TacAbstract (tc,Some s)
+(*End of To do*)
+      | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+	  TacFirst l
+      | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+	  TacSolve l
+      | IDENT "idtac" -> TacId
+      | IDENT "fail" -> TacFail fail_default_value
+      | IDENT "fail"; n = natural -> TacFail n
+      | st = simple_tactic -> TacAtom (loc,st)
+      | IDENT "eval"; rtc = red_expr; "in"; c = Constr.lconstr ->
+	  TacArg(ConstrMayEval (ConstrEval (rtc,c)))
+      | IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
+	  TacArg(ConstrMayEval (ConstrContext (id,c)))
+      | IDENT "check"; c = Constr.lconstr ->
+	  TacArg(ConstrMayEval (ConstrTypeOf c))
+      | "'"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c))
+      | r = reference; la = LIST1 tactic_arg ->
+          TacArg(TacCall (loc,r,la))
+      | r = reference -> TacArg (Reference r) ]
+    | "0"
+      [ "("; a = tactic_expr; ")" -> a
+      | a = tactic_atom -> TacArg a ] ]
+  ;
+  (* Tactic arguments *)
+  tactic_arg:
+    [ [ "'"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+      | a = tactic_atom -> a
+      | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ]
+  ;
+  tactic_atom:
+    [ [ id = METAIDENT -> MetaIdArg (loc,id)
+      | r = reference -> Reference r
+      | "?"; n = natural -> MetaNumArg (loc,n)
+      | "()" -> TacVoid ] ]
+  ;
+  input_fun:
+    [ [ IDENT "_" -> None 
+      | l = base_ident -> Some l ] ]
+  ;
+  let_clause:
+    [ [ id = identref; ":="; te = tactic_expr ->
+          LETCLAUSE (id, None, arg_of_expr te)
+      | (_,id) = identref; ":"; c = Constr.constr; ":="; IDENT "proof" ->
+          LETTOPCLAUSE (id, c)
+      | id = identref; ":"; c = constrarg; ":="; te = tactic_expr ->
+          LETCLAUSE (id, Some c, arg_of_expr te)
+      |	(_,id) = identref; ":"; c = Constr.lconstr ->
+	  LETTOPCLAUSE (id, c) ] ]
+  ;
+  rec_clause:
+    [ [ name = identref; it = LIST1 input_fun; "=>"; body = tactic_expr ->
+          (name,(it,body)) ] ]
+  ;
+  match_pattern:
+    [ [ id = Constr.constr_pattern; "["; pc = Constr.constr_pattern; "]" ->
+        let s = coerce_to_id id in Subterm (Some s, pc)
+      | "["; pc = Constr.constr_pattern; "]" -> Subterm (None,pc)
+      | pc = Constr.constr_pattern -> Term pc ] ]
+  ;
+  match_hyps:
+    [ [ id = identref; ":"; mp =  match_pattern -> Hyp (id, mp)
+      | IDENT "_"; ":"; mp = match_pattern -> NoHypId mp ] ]
+  ;
+  match_context_rule:
+    [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
+        "=>"; te = tactic_expr -> Pat (largs, mp, te)
+      | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+  ;
+  match_context_list:
+    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
+  ;
+  match_rule:
+    [ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te)
+      | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+  ;
+  match_list:
+    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
+  ;
+
+  (* Definitions for tactics *)
+  deftok:
+    [ [ IDENT "Meta"
+      | IDENT "Tactic" ] ]
+  ;
+  tacdef_body:
+    [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
+	  (name, TacFun (it, body))
+      | name = identref; ":="; body = tactic_expr ->
+	  (name, body) ] ]
+  ;
+  tactic:
+    [ [ tac = tactic_expr -> tac ] ]
+  ;
+  Vernac_.command: 
+    [ [ deftok; IDENT "Definition"; b = tacdef_body ->
+          VernacDeclareTacticDefinition (false, [b])
+      | IDENT "Recursive"; deftok; IDENT "Definition"; 
+        l = LIST1 tacdef_body SEP "with" ->
+          VernacDeclareTacticDefinition (true, l) ] ]
+  ;
+  END
diff --git a/parsing/g_natsyntaxnew.ml b/parsing/g_natsyntaxnew.ml
new file mode 100644
index 000000000..b124c4ec0
--- /dev/null
+++ b/parsing/g_natsyntaxnew.ml
@@ -0,0 +1,195 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* This file to allow writing (3) for (S (S (S O))) 
+   and still write (S y) for (S y) *)
+
+open Pcoq
+open Pp
+open Util
+open Names
+open Coqast
+open Ast
+open Coqlib
+open Termast
+open Extend
+(*
+let ast_O = ast_of_ref glob_O
+let ast_S = ast_of_ref glob_S
+
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+let nat_of_int n dloc =
+  let ast_O = set_loc dloc ast_O in
+  let ast_S = set_loc dloc ast_S in
+  let rec mk_nat n =
+    if n <= 0 then 
+      ast_O
+    else 
+      Node(dloc,"APPLIST", [ast_S; mk_nat (n-1)])
+  in 
+  mk_nat n
+
+let pat_nat_of_int n dloc =
+  let ast_O = set_loc dloc ast_O in
+  let ast_S = set_loc dloc ast_S in
+  let rec mk_nat n =
+    if n <= 0 then 
+      ast_O
+    else 
+      Node(dloc,"PATTCONSTRUCT", [ast_S; mk_nat (n-1)])
+  in 
+  mk_nat n
+
+let nat_of_string s dloc = 
+  nat_of_int (int_of_string s) dloc
+
+let pat_nat_of_string s dloc = 
+  pat_nat_of_int (int_of_string s) dloc
+    
+exception Non_closed_number
+
+let rec int_of_nat_rec astS astO p =
+  match p with
+    | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) ->
+	(int_of_nat_rec astS astO a)+1
+    | a when alpha_eq(a,astO) -> 1  
+          (***** YES, 1, non 0 ... to print the successor of p *)
+    | _ -> raise Non_closed_number
+	  
+let int_of_nat p =
+  try 
+    Some (int_of_nat_rec ast_S ast_O p)
+  with
+    Non_closed_number -> None
+
+let pr_S a = hov 0 (str "S" ++ brk (1,1) ++ a)
+
+let rec pr_external_S std_pr = function
+  | Node (l,"APPLIST", [b; a]) when alpha_eq (b,ast_S) ->
+      str"(" ++ pr_S (pr_external_S std_pr a) ++ str")"
+  | p -> std_pr p
+
+(* Declare the primitive printer *)
+
+(* Prints not p, but the SUCCESSOR of p !!!!! *)
+let nat_printer std_pr p =
+  match (int_of_nat p) with
+    | Some i -> str "(" ++ str (string_of_int i) ++ str ")"
+    | None -> str "(" ++ pr_S (pr_external_S std_pr p) ++ str ")"
+
+let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
+*)
+(*
+(* Declare the primitive parser *)
+
+let unat = create_univ_if_new "nat"
+
+let number = create_constr_entry unat "number" 
+let pat_number = create_constr_entry unat "pat_number"
+ 
+let _ = 
+  Gram.extend number None
+    [None, None,
+     [[Gramext.Stoken ("INT", "")],
+      Gramext.action nat_of_string]]
+
+let _ = 
+  Gram.extend pat_number None
+    [None, None,
+     [[Gramext.Stoken ("INT", "")],
+      Gramext.action pat_nat_of_string]]
+*)
+
+(*i*)
+open Rawterm
+open Libnames
+open Bignat
+open Coqlib
+open Symbols
+open Pp
+open Util
+open Names
+(*i*)
+
+(**********************************************************************)
+(* Parsing via scopes *)
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+
+let nat_of_int dloc n =
+  match n with
+  | POS n ->
+      if less_than (of_string "5000") n & Options.is_verbose () then begin
+	warning ("You may experiment stack overflow and segmentation fault\
+                  \nwhile parsing numbers in nat greater than 5000");
+	flush_all ()
+      end;
+      let ref_O = RRef (dloc, glob_O) in
+      let ref_S = RRef (dloc, glob_S) in
+      let rec mk_nat acc n =
+	if is_nonzero n then 
+	  mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n)
+	else 
+	  acc
+      in 
+      mk_nat ref_O n
+  | NEG n ->
+      user_err_loc (dloc, "nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+let pat_nat_of_int dloc n name =
+  match n with
+  | POS n -> 
+      let rec mk_nat n name =
+	if is_nonzero n then 
+	  PatCstr (dloc,path_of_S,[mk_nat (sub_1 n) Anonymous],name)
+	else 
+	  PatCstr (dloc,path_of_O,[],name)
+      in 
+      mk_nat n name
+  | NEG n ->
+      user_err_loc (dloc, "pat_nat_of_int",
+        str "Cannot interpret a negative number as a natural number")
+
+(***********************************************************************)
+(* Printing via scopes *)
+
+exception Non_closed_number
+
+let rec int_of_nat = function
+  | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a)
+  | RRef (_,z) when z = glob_O -> zero
+  | _ -> raise Non_closed_number
+	  
+let uninterp_nat p =
+  try 
+    Some (POS (int_of_nat p))
+  with
+    Non_closed_number -> None
+
+let rec int_of_nat_pattern = function
+  | PatCstr (_,s,[a],_) when ConstructRef s = glob_S ->
+      add_1 (int_of_nat_pattern a)
+  | PatCstr (_,z,[],_) when ConstructRef z = glob_O -> zero
+  | _ -> raise Non_closed_number
+	  
+let uninterp_nat_pattern p =
+  try 
+    Some (POS (int_of_nat_pattern p))
+  with
+    Non_closed_number -> None
+
+(***********************************************************************)
+(* Declare the primitive parsers and printers *)
+
+let _ =
+  Symbols.declare_numeral_interpreter "nat_scope"
+    ["Coq";"Init";"Peano"]
+    (nat_of_int,Some pat_nat_of_int)
+    ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
diff --git a/parsing/g_natsyntaxnew.mli b/parsing/g_natsyntaxnew.mli
new file mode 100644
index 000000000..91596ef5c
--- /dev/null
+++ b/parsing/g_natsyntaxnew.mli
@@ -0,0 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(* Nice syntax for naturals. *)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 9dd073cfd..39a7687f1 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -19,6 +19,8 @@ open Qast
 
 open Prim
 
+let _ = reset_all_grammars()
+
 (* camlp4o pa_extend.cmo pa_extend_m.cmo pr_o.cmo q_prim.ml *)
 
 ifdef Quotify then
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
new file mode 100644
index 000000000..de18ab764
--- /dev/null
+++ b/parsing/g_primnew.ml4
@@ -0,0 +1,143 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Coqast
+open Pcoq
+open Names
+open Libnames
+open Topconstr
+
+let _ = Pcoq.reset_all_grammars()
+let _ =
+  let f = Gram.Unsafe.clear_entry in
+  f Prim.bigint;
+  f Prim.qualid;
+  f Prim.ast;
+  f Prim.reference
+
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'";"."]
+let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw
+
+ifdef Quotify then
+open Qast
+
+open Prim
+
+ifdef Quotify then
+module Prelude = struct
+let local_id_of_string s = Apply ("Names","id_of_string", [s])
+let local_make_dirpath l = Qast.Apply ("Names","make_dirpath",[l])
+let local_make_posint s = s
+let local_make_negint s = Apply ("Pervasives","~-", [s])
+let local_make_qualid l id' = 
+  Qast.Apply ("Nametab","make_qualid", [local_make_dirpath l;id'])
+let local_make_short_qualid id =
+  Qast.Apply ("Nametab","make_short_qualid",[id])
+let local_make_path l id' =
+  Qast.Apply ("Libnames","encode_kn", [local_make_dirpath l;id'])
+let local_make_binding loc a b =
+  match a with
+    | Qast.Node ("Nvar", [_;id]) ->
+	Qast.Node ("Slam", [Qast.Loc; Qast.Option (Some id); b])
+    | Qast.Node ("Nmeta", [_;s]) ->
+	Qast.Node ("Smetalam", [Qast.Loc;s;b])
+    | _ -> 
+	Qast.Apply ("Pervasives", "failwith", [Qast.Str "Slam expects a var or a metavar"])
+let local_append l id = Qast.Apply ("List","append", [l; Qast.List [id]])
+end
+
+else
+
+module Prelude = struct
+open Nametab
+let local_id_of_string = id_of_string
+let local_make_dirpath = make_dirpath
+let local_make_qualid l id' = make_qualid (local_make_dirpath l) id'
+let local_make_short_qualid id = make_short_qualid id
+let local_make_posint = int_of_string
+let local_make_negint n = - int_of_string n
+let local_make_path l a = encode_kn (local_make_dirpath l) a
+let local_make_binding loc a b =
+  match a with
+    | Nvar (_,id) -> Slam(loc,Some id,b)
+    | Nmeta (_,s) -> Smetalam(loc,s,b)
+    | _ -> failwith "Slam expects a var or a metavar"
+let local_append l id = l@[id]
+end
+
+open Prelude
+
+ifdef Quotify then
+open Q
+
+GEXTEND Gram
+  GLOBAL: ast bigint qualid reference;
+  metaident:
+    [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
+  ;
+  field:
+    [ [ "."; s = IDENT -> local_id_of_string s ] ]
+  ;
+  fields:
+    [ [ id = field; (l,id') = fields -> (local_append l id,id')
+      | id = field -> ([],id)
+      ] ]
+  ;
+  astpath:
+    [ [ id = base_ident; (l,a) = fields ->
+          Path(loc, local_make_path (local_append l id) a)
+      | id = base_ident -> Nvar(loc, id)
+      ] ]
+  ;
+  basequalid:
+    [ [ id = base_ident; (l,id')=fields ->
+          local_make_qualid (local_append l id) id'
+      | id = base_ident -> local_make_short_qualid id
+      ] ]
+  ;
+  reference:
+    [ [ id = base_ident; (l,id') = fields ->
+        Qualid (loc, local_make_qualid (local_append l id) id')
+      | id = base_ident -> Ident (loc,id)
+      ] ]
+  ;
+  qualid:
+    [ [ qid = basequalid -> loc, qid ] ]
+  ;
+  ast:
+    [ [ id = metaident -> id
+      | p = astpath -> p
+      | s = INT -> Num(loc, local_make_posint s)
+      | s = STRING -> Str(loc, s)
+      | "{"; s = METAIDENT; "}" -> Id(loc,s)
+      | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
+      | "("; METAIDENT "$LIST"; id = metaident; ")" -> Node(loc,"$LIST",[id])
+      | "("; METAIDENT "$STR"; id = metaident; ")" -> Node(loc,"$STR",[id])
+      | "("; METAIDENT "$VAR"; id = metaident; ")" -> Node(loc,"$VAR",[id])
+      | "("; METAIDENT "$ID"; id = metaident; ")" -> Node(loc,"$ID",[id])
+      | "("; METAIDENT "$ABSTRACT"; l = LIST0 ast;")"->Node(loc,"$ABSTRACT",l)
+      | "("; METAIDENT "$PATH"; id = metaident; ")" -> Node(loc,"$PATH",[id])
+      | "("; METAIDENT "$NUM"; id = metaident; ")" -> Node(loc,"$NUM",[id])
+      | "["; "<>"; "]"; b = ast -> Slam(loc,None,b)
+      | "["; a = ast; "]"; b = ast -> local_make_binding loc a b
+      | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
+  ;
+  bigint: (* Negative numbers are dealt with specially *)
+    [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
+  ;
+END
+
+let constr_to_ast a =
+  Termast.ast_of_rawconstr
+    (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
+
+let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
+
+let _ = define_ast_quotation true "constr" constr_parser_with_glob
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 879ce98ae..f6801bf31 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -18,6 +18,8 @@ open Vernacexpr
 open Prim
 open Constr
 
+let thm_token = Gram.Entry.create "vernac:thm_token"
+
 (* Proof commands *)
 GEXTEND Gram
   GLOBAL: command;
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
new file mode 100644
index 000000000..db8da7101
--- /dev/null
+++ b/parsing/g_proofsnew.ml4
@@ -0,0 +1,126 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pcoq
+open Pp
+open Tactic
+open Util
+open Vernac_
+open Topconstr
+open Vernacexpr
+open Prim
+open Constr
+
+let thm_token = G_vernacnew.thm_token
+
+(* Proof commands *)
+GEXTEND Gram
+  GLOBAL: command;
+
+  destruct_location :
+  [ [ IDENT "Conclusion"  -> Tacexpr.ConclLocation ()
+    | discard = [ IDENT "Discardable" -> true | -> false ]; IDENT "Hypothesis"
+	-> Tacexpr.HypLocation discard ] ]
+  ;
+  opt_hintbases:
+  [ [ -> []
+    | ":"; l = LIST1 IDENT -> l ] ]
+  ;
+  command:
+    [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c
+      | IDENT "Proof" -> VernacNop
+      | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
+      | IDENT "Abort" -> VernacAbort None
+      | IDENT "Abort"; IDENT "All" -> VernacAbortAll
+      | IDENT "Abort"; id = identref -> VernacAbort (Some id)
+      | IDENT "Existential"; n = natural; c = constr_body ->
+	  VernacSolveExistential (n,c)
+      | IDENT "Qed" -> VernacEndProof (true,None)
+      | IDENT "Save" -> VernacEndProof (true,None)
+      | IDENT "Save"; tok = thm_token; id = base_ident ->
+	  VernacEndProof (true,Some (id,Some tok))
+      | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None))
+      | IDENT "Defined" -> VernacEndProof (false,None)
+      |	IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None))
+      | IDENT "Suspend" -> VernacSuspend
+      | IDENT "Resume" -> VernacResume None
+      | IDENT "Resume"; id = identref -> VernacResume (Some id)
+      | IDENT "Restart" -> VernacRestart
+      | IDENT "Proof"; c = Constr.lconstr -> VernacExactProof c
+      | IDENT "Undo" -> VernacUndo 1
+      | IDENT "Undo"; n = natural -> VernacUndo n
+      | IDENT "Focus" -> VernacFocus None
+      | IDENT "Focus"; n = natural -> VernacFocus (Some n)
+      | IDENT "Unfocus" -> VernacUnfocus
+      | IDENT "Show" -> VernacShow (ShowGoal None)
+      | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
+      | IDENT "Show"; IDENT "Implicits"; n = natural ->
+	  VernacShow (ShowGoalImplicitly (Some n))
+      | IDENT "Show"; IDENT "Implicits" -> VernacShow (ShowGoalImplicitly None)
+      | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
+      | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
+      | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
+      | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree
+      | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
+      | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
+      | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
+      | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
+      | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
+	  VernacShow (ExplainProof l)
+      | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> 
+	  VernacShow (ExplainTree l)
+      | IDENT "Go"; n = natural -> VernacGo (GoTo n)
+      | IDENT "Go"; IDENT "top" -> VernacGo GoTop
+      | IDENT "Go"; IDENT "prev" -> VernacGo GoPrev
+      | IDENT "Go"; IDENT "next" -> VernacGo GoNext
+      | IDENT "Guarded" -> VernacCheckGuard
+(* Hints for Auto and EAuto *)
+
+      | IDENT "HintDestruct"; 
+          dloc = destruct_location;
+          id  = base_ident;
+          hyptyp = Constr.constr_pattern;
+          pri = natural;
+          "["; tac = tactic; "]" -> 
+	    VernacHintDestruct (id,dloc,hyptyp,pri,tac)
+
+      | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint
+          -> VernacHints (dbnames, h hintname)
+	  
+      | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h)
+	  
+
+(*This entry is not commented, only for debug*)
+      | IDENT "PrintConstr"; c = Constr.constr -> 
+	  VernacExtend ("PrintConstr",
+	    [Genarg.in_gen Genarg.rawwit_constr c])
+      ] ];
+
+  hint:
+    [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
+      | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
+      | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
+      | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c)
+      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
+	  fun name -> HintsExtern (name,n,c,tac) ] ]
+  ;
+  hints:
+    [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
+         (dbnames, HintsResolve (List.map (fun qid -> (None, CRef qid)) l))
+      | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
+        (dbnames, HintsImmediate (List.map (fun qid -> (None, CRef qid)) l))
+      | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
+        (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
+    ;
+  constr_body:
+    [ [ ":="; c = lconstr -> c
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,t) ] ]
+  ;
+END
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 6edbf7c55..13eb76334 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -66,7 +66,13 @@ let r_of_int n dloc =
 let r_of_string s dloc = 
   r_of_int (int_of_string s) dloc
 
-let rnumber = create_constr_entry (get_univ "rnatural") "rnumber"
+let rsyntax_create name =
+  let e =
+    Pcoq.create_constr_entry (Pcoq.get_univ "rnatural") name in
+  Pcoq.Gram.Unsafe.clear_entry e;
+  e
+
+let rnumber = rsyntax_create "rnumber"
 
 let _ = 
   Gram.extend rnumber None
diff --git a/parsing/g_rsyntaxnew.ml b/parsing/g_rsyntaxnew.ml
new file mode 100644
index 000000000..081762ae3
--- /dev/null
+++ b/parsing/g_rsyntaxnew.ml
@@ -0,0 +1,113 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+open Coqast
+open Ast
+open Pp
+open Util
+open Names
+open Pcoq
+open Extend
+open Topconstr
+open Libnames
+
+(**********************************************************************)
+(* Parsing R via scopes                                               *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+open Bignat
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir (id_of_string id)
+
+let glob_R1 = ConstRef (make_path rdefinitions "R1")
+let glob_R0 = ConstRef (make_path rdefinitions "R0")
+let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
+let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
+let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
+
+let two = mult_2 one
+let three = add_1 two
+let four = mult_2 two
+
+(* Unary representation of strictly positive numbers *)
+let rec small_r dloc n =
+  if is_one n then RRef (dloc, glob_R1)
+  else RApp(dloc,RRef (dloc,glob_Rplus),
+            [RRef (dloc, glob_R1);small_r dloc (sub_1 n)])
+
+let r_of_posint dloc n =
+  let r1 = RRef (dloc, glob_R1) in
+  let r2 = small_r dloc two in
+  let rec r_of_pos n =
+    if less_than n four then small_r dloc n
+    else
+      let (q,r) = div2_with_rest n in
+      let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
+      if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in
+  if is_nonzero n then r_of_pos n else RRef(dloc,glob_R0)
+
+let r_of_int dloc z =
+  match z with
+  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
+  | POS n -> r_of_posint dloc n
+
+(**********************************************************************)
+(* Printing R via scopes                                              *)
+(**********************************************************************)
+
+exception Non_closed_number
+
+(* for numbers > 1 *)
+let rec bignat_of_pos = function
+  (* 1+1 *)
+  | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)])
+      when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two
+  (* 1+1+1 *)
+  | RApp (_,RRef (_,p1), [RRef (_,o1);
+      RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])])
+      when p1 = glob_Rplus & p2 = glob_Rplus &
+           o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three
+  (* (1+1)*b *)
+  | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult ->
+      if bignat_of_pos a <> two then raise Non_closed_number;
+      mult_2 (bignat_of_pos b)
+  (* 1+(1+1)*b *)
+  | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])])
+      when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1  -> 
+      if bignat_of_pos a <> two then raise Non_closed_number;
+        add_1 (mult_2 (bignat_of_pos b))
+  | _ -> raise Non_closed_number
+
+let bignat_of_r = function
+  | RRef (_,a) when a = glob_R0 -> zero
+  | RRef (_,a) when a = glob_R1 -> one
+  | r -> bignat_of_pos r
+
+let bigint_of_r = function
+  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
+  | a -> POS (bignat_of_r a)
+
+let uninterp_r p =
+  try
+    Some (bigint_of_r p)
+  with Non_closed_number ->
+    None
+
+let _ = Symbols.declare_numeral_interpreter "R_scope"
+  ["Coq";"Reals";"Rsyntax"]
+  (r_of_int,None)
+  ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
+    RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult);RRef(dummy_loc,glob_R1)],
+    uninterp_r,
+    None)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c7f8217d1..fe77a3095 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -22,6 +22,10 @@ open Constr
 open Prim
 open Tactic
 
+let tactic_kw =
+  [ "using"; "Orelse"; "Proof"; "Qed"; "And"; "()"; "|-" ]
+let _ = List.iter (fun s -> Lexer.add_token ("",s)) tactic_kw
+
 (* Functions overloaded by quotifier *)
 
 let induction_arg_of_constr c =
@@ -319,9 +323,9 @@ GEXTEND Gram
       (* Constructors *)
       | IDENT "Left"; bl = with_binding_list -> TacLeft bl
       | IDENT "Right"; bl = with_binding_list -> TacRight bl
-      | IDENT "Split"; bl = with_binding_list -> TacSplit bl
-      | IDENT "Exists"; bl = binding_list -> TacSplit bl
-      | IDENT "Exists" -> TacSplit NoBindings
+      | IDENT "Split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "Exists"; bl = binding_list -> TacSplit (true,bl)
+      | IDENT "Exists" -> TacSplit (true,NoBindings)
       | IDENT "Constructor"; n = num_or_meta; l = with_binding_list ->
 	  TacConstructor (n,l)
       | IDENT "Constructor"; t = OPT tactic -> TacAnyConstructor t
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
new file mode 100644
index 000000000..4083fe82c
--- /dev/null
+++ b/parsing/g_tacticnew.ml4
@@ -0,0 +1,355 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Ast
+open Pcoq
+open Util
+open Tacexpr
+open Rawterm
+
+let tactic_kw =
+  [ "->"; "<-" ]
+let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
+
+(* Hack to parse "with n := c ..." as a binder without conflicts with the *)
+(* admissible notation "with c1 c2..." *)
+let test_coloneq2 =
+  Gram.Entry.of_parser "test_int_coloneq"
+    (fun strm ->
+      match Stream.npeek 2 strm with
+        | [_; ("", ":=")] -> ()
+        | _ -> raise Stream.Failure)
+
+(* open grammar entries, possibly in quotified form *)
+ifdef Quotify then open Qast
+
+open Constr
+open Prim
+open Tactic
+
+(* Functions overloaded by quotifier *)
+
+let induction_arg_of_constr c =
+  try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c
+
+let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
+
+let error_oldelim _ = error "OldElim no longer supported"
+
+ifdef Quotify then
+  let induction_arg_of_constr = function
+  | Qast.Node ("Nvar", [_;id]) -> Qast.Node ("ElimOnIdent", [id])
+  | c -> Qast.Node ("ElimOnConstr", [c])
+
+ifdef Quotify then
+let make_red_flag s = Qast.Apply ("make_red_flag", [s])
+
+ifdef Quotify then
+let local_compute = 
+  Qast.List [
+    Qast.Node ("FBeta", []);
+    Qast.Node ("FDeltaBut", [Qast.List []]);
+    Qast.Node ("FIota", []);
+    Qast.Node ("FZeta", [])]
+
+ifdef Quotify then open Q
+
+let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
+
+(* Auxiliary grammar rules *)
+
+GEXTEND Gram
+  GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
+    red_expr int_or_var castedopenconstr;
+
+  int_or_var:
+    [ [ n = integer  -> Genarg.ArgArg n
+      | id = identref -> Genarg.ArgVar id ] ]
+  ;
+  autoarg_depth:
+  [ [ n = OPT natural -> n ] ]
+  ;
+  autoarg_adding:
+  [ [ IDENT "adding" ; "["; l = LIST1 global; "]" -> l | -> [] ] ]
+  ;
+  autoarg_destructing:
+  [ [ IDENT "destructing" -> true | -> false ] ]
+  ;
+  autoarg_usingTDB:
+  [ [ "using"; "tdb"  -> true | -> false ] ]
+  ;
+  autoargs:
+  [ [ a0 = autoarg_depth; l = autoarg_adding; 
+      a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ]
+  ;
+  (* Either an hypothesis or a ltac ref (variable or pattern metavariable) *)
+  id_or_ltac_ref:
+    [ [ id = base_ident -> AN id
+      | "?"; n = natural -> MetaNum (loc,n) ] ]
+  ;
+  (* Either a global ref or a ltac ref (variable or pattern metavariable) *)
+  global_or_ltac_ref:
+    [ [ qid = global -> AN qid
+      | "?"; n = natural -> MetaNum (loc,n) ] ]
+  ;
+  (* An identifier or a quotation meta-variable *)
+  id_or_meta:
+    [ [ id = identref -> AI id 
+
+      (* This is used in quotations *)
+      | id = METAIDENT -> MetaId (loc,id) ] ]
+  ;
+  (* A number or a quotation meta-variable *)
+  num_or_meta:
+    [ [ n = integer -> AI n
+      |	id = METAIDENT -> MetaId (loc,id)
+      ] ]
+  ;
+  constrarg:
+    [ [ IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
+        ConstrContext (id, c)
+      | IDENT "eval"; rtc = Tactic.red_expr; "in"; c = Constr.lconstr ->
+        ConstrEval (rtc,c) 
+      | IDENT "check"; c = Constr.lconstr -> ConstrTypeOf c
+      | c = Constr.lconstr -> ConstrTerm c ] ]
+  ;
+  castedopenconstr:
+    [ [ c = lconstr -> c ] ]
+  ;
+  induction_arg:
+    [ [ n = natural -> ElimOnAnonHyp n
+      | c = lconstr -> induction_arg_of_constr c
+    ] ]
+  ;
+  quantified_hypothesis:
+    [ [ id = base_ident -> NamedHyp id
+      | n = natural -> AnonHyp n ] ]
+  ;
+  conversion:
+    [ [ nl = LIST1 integer; c1 = constr; "with"; c2 = constr ->
+         (Some (nl,c1), c2)
+      |	c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
+      | c = constr -> (None, c) ] ]
+  ;
+  pattern_occ:
+    [ [ nl = LIST0 integer; c = [c=constr->c | g=global->Topconstr.CRef g]-> (nl,c) ] ]
+  ;
+  pattern_occ_hyp_list:
+    [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[])
+      | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_list ->
+	  (g,(id,nl)::l)
+      | IDENT "Goal" -> (Some [],[])
+      | id = id_or_meta; (g,l) = pattern_occ_hyp_list -> (g,(id,[])::l) ] ]
+  ;
+  clause_pattern:
+    [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ]
+  ;
+  intropatterns:
+    [ [ l = LIST0 simple_intropattern -> l ]]
+  ;
+  simple_intropattern:
+    [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
+      | "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
+      | IDENT "_" -> IntroWildcard
+      | id = base_ident -> IntroIdentifier id
+      ] ]
+  ;
+  simple_binding:
+    [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c)
+      | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ]
+  ;
+  binding_list:
+    [ [ test_coloneq2; n = natural; ":="; c = constr;
+        bl = LIST0 simple_binding ->
+	  ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl)
+      | test_coloneq2; id = base_ident; ":="; c2 = constr;
+        bl = LIST0 simple_binding ->
+          ExplicitBindings
+            ((join_to_constr loc c2,NamedHyp id, c2) :: bl)
+      | c1 = constr; bl = LIST0 constr ->
+	  ImplicitBindings (c1 :: bl) ] ]
+  ;
+  constr_with_bindings:
+    [ [ c = constr; l = with_binding_list -> (c, l) ] ]
+  ;
+  with_binding_list:
+    [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
+  ;
+  unfold_occ:
+    [ [ nl = LIST0 integer; c = global_or_ltac_ref -> (nl,c) ] ]
+  ;
+  red_flag:
+    [ [ IDENT "beta" -> FBeta
+      | IDENT "delta" -> FDeltaBut []
+      | IDENT "iota" -> FIota
+      | IDENT "zeta" -> FZeta
+      | IDENT "delta"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FConst idl
+      | IDENT "delta"; "-"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FDeltaBut idl
+    ] ]
+  ;
+  red_tactic:
+    [ [ IDENT "red" -> Red false
+      | IDENT "hnf" -> Hnf
+      | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+      | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
+      | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
+      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
+      | IDENT "fold"; cl = LIST1 constr -> Fold cl
+      | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ]
+  ;
+  (* This is [red_tactic] including possible extensions *)
+  red_expr:
+    [ [ IDENT "red" -> Red false
+      | IDENT "hnf" -> Hnf
+      | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
+      | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
+      | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
+      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
+      | IDENT "fold"; cl = LIST1 constr -> Fold cl
+      | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
+      | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+  ;
+  hypident:
+    [ [ id = id_or_meta -> InHyp id
+      | "("; "type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
+  ;
+  clause:
+    [ [ "in"; idl = LIST1 hypident -> idl
+      | -> [] ] ]
+  ;
+  fixdecl:
+    [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
+  ;
+  cofixdecl:
+    [ [ id = base_ident; ":"; c = constr -> (id,c) ] ]
+  ;
+  hintbases:
+    [ [ "with"; "*" -> None
+      | "with"; l = LIST1 IDENT -> Some l
+      | -> Some [] ] ]
+  ;
+  eliminator:
+    [ [ "using"; el = constr_with_bindings -> el ] ]
+  ;
+  with_names:
+    [ [ "as"; "["; ids = LIST1 (LIST0 base_ident) SEP "|"; "]" -> ids
+      | -> [] ] ]
+  ;
+  simple_tactic:
+    [ [ 
+      (* Basic tactics *)
+        IDENT "intros"; IDENT "until"; id = quantified_hypothesis -> 
+	  TacIntrosUntil id
+      | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl
+      | IDENT "intro"; id = base_ident; IDENT "after"; id2 = identref ->
+	  TacIntroMove (Some id, Some id2)
+      | IDENT "intro"; IDENT "after"; id2 = identref ->
+	  TacIntroMove (None, Some id2)
+      | IDENT "intro"; id = base_ident -> TacIntroMove (Some id, None)
+      | IDENT "intro" -> TacIntroMove (None, None)
+
+      | IDENT "assumption" -> TacAssumption
+      | IDENT "exact"; c = lconstr -> TacExact c
+
+      | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
+      | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
+          TacElim (cl,el)
+      | IDENT "elimtype"; c = lconstr -> TacElimType c
+      | IDENT "case"; cl = constr_with_bindings -> TacCase cl
+      | IDENT "casetype"; c = lconstr -> TacCaseType c
+      | "fix"; n = natural -> TacFix (None,n)
+      | "fix"; id = base_ident; n = natural -> TacFix (Some id,n)
+      | "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl ->
+	  TacMutualFix (id,n,fd)
+      | "cofix" -> TacCofix None
+      | "cofix"; id = base_ident -> TacCofix (Some id)
+      | "cofix"; id = base_ident; "with"; fd = LIST0 cofixdecl ->
+	  TacMutualCofix (id,fd)
+
+      | IDENT "cut"; c = lconstr -> TacCut c
+      | IDENT "assert"; c = lconstr ->
+          (match c with
+              Topconstr.CCast(_,c,t) -> TacTrueCut (Some (coerce_to_id c),t)
+            | _ -> TacTrueCut (None,c))
+      | IDENT "assert"; c = lconstr; ":="; b = lconstr ->
+          TacForward (false,Names.Name (coerce_to_id c),b)
+      | IDENT "pose"; c = lconstr; ":="; b = lconstr ->
+	  TacForward (true,Names.Name (coerce_to_id c),b)
+      | IDENT "pose"; b = lconstr -> TacForward (true,Names.Anonymous,b)
+      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
+      | IDENT "generalize"; IDENT "dependent"; c = lconstr ->
+          TacGeneralizeDep c
+      | IDENT "lettac"; id = base_ident; ":="; c = lconstr; p = clause_pattern
+        -> TacLetTac (id,c,p)
+      | IDENT "instantiate"; n = natural; c = lconstr -> TacInstantiate (n,c)
+
+      | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
+	  TacSpecialize (n,lcb)
+      | IDENT "lapply"; c = lconstr -> TacLApply c
+
+      (* Derived basic tactics *)
+      | IDENT "induction"; h = quantified_hypothesis -> TacOldInduction h
+      | IDENT "newinduction"; c = induction_arg; el = OPT eliminator;
+          ids = with_names -> TacNewInduction (c,el,ids)
+      | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
+	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
+      | IDENT "destruct"; h = quantified_hypothesis -> TacOldDestruct h
+      | IDENT "newdestruct"; c = induction_arg; el = OPT eliminator; 
+          ids = with_names -> TacNewDestruct (c,el,ids)
+      | IDENT "decompose"; IDENT "record" ; c = lconstr -> TacDecomposeAnd c
+      | IDENT "decompose"; IDENT "sum"; c = lconstr -> TacDecomposeOr c
+      | IDENT "decompose"; "["; l = LIST1 global_or_ltac_ref; "]"; c = lconstr
+        -> TacDecompose (l,c)
+
+      (* Automation tactic *)
+      | IDENT "trivial"; db = hintbases -> TacTrivial db
+      | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+
+      | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
+      | IDENT "cdhyp"; id = identref -> TacDestructHyp (true,id)
+      | IDENT "dhyp";  id = identref -> TacDestructHyp (false,id)
+      | IDENT "dconcl"  -> TacDestructConcl
+      | IDENT "superauto"; l = autoargs -> TacSuperAuto l
+      | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
+	  TacDAuto (n, p)
+
+      (* Context management *)
+      | IDENT "clear"; l = LIST1 id_or_ltac_ref -> TacClear l
+      | IDENT "clearbody"; l = LIST1 id_or_ltac_ref -> TacClearBody l
+      | IDENT "move"; id1 = identref; IDENT "after"; id2 = identref -> 
+	  TacMove (true,id1,id2)
+      | IDENT "rename"; id1 = identref; IDENT "into"; id2 = identref -> 
+	  TacRename (id1,id2)
+
+      (* Constructors *)
+      | IDENT "left"; bl = with_binding_list -> TacLeft bl
+      | IDENT "right"; bl = with_binding_list -> TacRight bl
+      | IDENT "split"; bl = with_binding_list -> TacSplit (false,bl)
+      | IDENT "exists"; bl = binding_list -> TacSplit (true,bl)
+      | IDENT "exists" -> TacSplit (true,NoBindings)
+      | IDENT "constructor"; n = num_or_meta; l = with_binding_list ->
+	  TacConstructor (n,l)
+      | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor t
+
+      (* Equivalence relations *)
+      | IDENT "reflexivity" -> TacReflexivity
+      | IDENT "symmetry" -> TacSymmetry
+      | IDENT "transitivity"; c = lconstr -> TacTransitivity c
+
+      (* Conversion *)
+      | r = red_tactic; cl = clause -> TacReduce (r, cl)
+      (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
+      | IDENT "change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
+    ] ]
+  ;
+END;;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 68e6fe858..a082772ac 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -27,6 +27,9 @@ open Genarg
 
 let evar_constr loc = CHole loc
 
+let class_rawexpr = G_basevernac.class_rawexpr
+let thm_token = G_proofs.thm_token
+
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
@@ -325,15 +328,13 @@ GEXTEND Gram
       | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ]
   ;
 
-  module_vardecls: (* This is interpreted by Pcoq.abstract_binder *)
-    [ [ id = base_ident; idl = ident_comma_list_tail; ":"; mty = Module.module_type
+  module_vardecls:
+    [ [ "("; id = base_ident; idl = ident_comma_list_tail;
+        ":"; mty = Module.module_type; ")"
         -> (id::idl,mty) ] ]
   ;
-  module_binders:
-    [ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ]
-  ;
   module_binders_list:
-    [ [ bls = LIST0 module_binders -> List.flatten bls ] ]
+    [ [ bl = LIST0 module_vardecls -> bl ] ]
   ;
   of_module_type:
     [ [ ":"; mty = Module.module_type -> (mty, true) 
@@ -417,7 +418,7 @@ GEXTEND Gram
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,c,l)
 	     | None -> c in
-	   VernacNotation ("'"^id^"'",c,[],None)
+	   VernacNotation ("'"^id^"'",c,[],None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
@@ -474,7 +475,7 @@ GEXTEND Gram
 	  VernacRequireFrom (export, specif, id, filename) *)
       | IDENT "Require"; export = export_token; specif = specif_token;
         filename = STRING -> 
-	  VernacRequireFrom (export, specif, filename)
+	  VernacRequireFrom (Some export, specif, filename)
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
 	  VernacDeclareMLModule l
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
new file mode 100644
index 000000000..e88e97141
--- /dev/null
+++ b/parsing/g_vernacnew.ml4
@@ -0,0 +1,817 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Coqast
+open Topconstr
+open Vernacexpr
+open Pcoq
+open Tactic
+open Decl_kinds
+open Genarg
+open Extend
+open Ppextend
+open Goptions
+
+open Prim
+open Constr
+open Vernac_
+open Module
+
+
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:" ]
+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 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"
+
+GEXTEND Gram
+  GLOBAL: vernac gallina_ext;
+  vernac:
+    (* Better to parse ";" here: in case of failure (e.g. in coerce_to_var), *)
+    (* ";" is still in the stream and discard_to_dot works correctly         *)
+    [ [ g = gallina; ";" -> g 
+      | g = gallina_ext; ";" -> g
+      | c = command; ";" -> c 
+      | c = syntax; ";" -> c
+      | "["; l = LIST1 located_vernac; "]"; ";" -> VernacList l
+    ] ]
+  ;
+  vernac: FIRST
+    [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
+  ;
+  vernac: LAST
+    [ [ gln = OPT[n=natural; ":" -> n];
+        tac = subgoal_command; ";" -> tac gln ] ]
+  ;
+  subgoal_command:
+    [ [ c = check_command -> c
+      | d = use_default_tac; tac = Tactic.tactic ->
+          (fun g ->
+            let g = match g with Some gl -> gl | _ -> 1 in
+            VernacSolve(g,tac,d)) ] ]
+  ;
+  located_vernac:
+    [ [ v = vernac -> loc, v ] ]
+  ;
+  use_default_tac:
+    [ [ "!!" -> false 
+      | -> true ] ]
+  ;
+END
+
+
+let test_plurial_form = function
+  | [_] ->
+      Options.if_verbose warning
+   "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 *)
+GEXTEND Gram
+  GLOBAL: gallina gallina_ext thm_token def_body;
+
+  gallina:
+      (* Definition, Theorem, Variable, Axiom, ... *)
+    [ [ thm = thm_token; id = base_ident; bl = LIST0 binder; ":";
+        c = lconstr ->
+          VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
+      | (f,d,e) = def_token; id = base_ident; b = def_body -> 
+          VernacDefinition (d, id, b, f, e)
+      | stre = assumption_token; bl = LIST1 simple_binder_coe -> 
+	  VernacAssumption (stre, bl)
+      | stre = assumptions_token; bl = LIST1 simple_binder_coe ->
+	  test_plurial_form bl;
+	  VernacAssumption (stre, bl)
+      (* Gallina inductive declarations *)
+      | OPT[IDENT "Mutual"]; f = finite_token;
+        indl = LIST1 inductive_definition SEP "with" ->
+          VernacInductive (f,indl)
+      | IDENT "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint recs
+      | IDENT "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint corecs
+      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
+  ;
+  gallina_ext:
+    [ [ record_token; oc = opt_coercion; name = base_ident;
+        ps = LIST0 simple_binder; ":";
+	s = lconstr; ":="; cstr = OPT base_ident; "{";
+        fs = LIST0 local_decl_expr; "}" ->
+	  VernacRecord ((oc,name),ps,s,cstr,fs)
+      | f = finite_token; s = csort; id = base_ident;
+        indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
+          VernacInductive (f,[id,indpar,s,lc])
+    ] ]
+  ;
+  thm_token:
+    [ [ IDENT "Theorem" -> Theorem
+      | IDENT "Lemma" -> Lemma
+      | IDENT "Fact" -> Fact
+      | IDENT "Remark" -> Remark ] ]
+  ;
+  def_token:
+    [ [ IDENT "Definition" -> (fun _ _ -> ()), Global, GDefinition
+      | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition
+      | IDENT "SubClass"  -> Class.add_subclass_hook, Global, GCoercion
+      | IDENT "Local"; IDENT "SubClass"  ->
+          Class.add_subclass_hook, Local, LCoercion ] ] 
+  ;
+  assumption_token:
+    [ [ IDENT "Hypothesis" -> (Local, Logical)
+      | IDENT "Variable" -> (Local, Definitional)
+      | IDENT "Axiom" -> (Global, Logical)
+      | IDENT "Parameter" -> (Global, Definitional) ] ]
+  ;
+  assumptions_token:
+    [ [ IDENT "Hypotheses" -> (Local, Logical)
+      | IDENT "Variables" -> (Local, Definitional)
+      | IDENT "Parameters" -> (Global, Definitional) ] ]
+  ;
+  finite_token:
+    [ [ IDENT "Inductive" -> true
+      | IDENT "CoInductive" -> false ] ]
+  ;
+  record_token:
+    [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ]
+  ;
+  (* Simple definitions *)
+  def_body:
+    [ [ bl = LIST0 binder; ":="; red = reduce; c = lconstr ->
+      (match c with
+          CCast(_,c,t) -> DefineBody (bl, red, c, Some t)
+        | _ -> DefineBody (bl, red, c, None))
+      | bl = LIST0 binder; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+          DefineBody (bl, red, c, Some t)
+      | bl = LIST0 binder; ":"; t = lconstr ->
+          ProveBody (bl, t) ] ]
+  ;
+  reduce:
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
+      | -> None ] ]
+  ;
+  (* Inductives and records *)
+  inductive_definition:
+    [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":=";
+	lc = constructor_list -> (id,indpar,c,lc) ] ]
+  ;
+  constructor_list:
+    [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l
+      | l = LIST1 constructor_binder SEP "|" -> l
+      |  -> [] ] ]
+  ;
+  csort:
+    [ [ s = sort -> CSort (loc,s) ] ]
+  ;
+  opt_coercion:
+    [ [ ">" -> true
+      |  -> false ] ]
+  ;
+  (* (co)-fixpoints *)
+  rec_definition:
+    [ [ id = base_ident; bl = LIST1 binder_nodef; ":"; type_ = lconstr;
+        ":="; def = lconstr ->
+          let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+          let loc0 = fst (List.hd (fst (List.hd bl))) in
+          let loc1 = join_loc loc0 (constr_loc type_) in
+          let loc2 = join_loc loc0 (constr_loc def) in
+	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+  ;
+  corec_definition:
+    [ [ id = base_ident; ":"; c = lconstr; ":="; def = lconstr ->
+          (id,c,def) ] ]
+  ;
+  (* Inductive schemes *)
+  scheme:
+    [ [ id = base_ident; ":="; dep = dep_scheme; "for"; ind = global;
+        IDENT "Sort"; s = sort ->
+          (id,dep,ind,s) ] ]
+  ;
+  dep_scheme:
+    [ [ IDENT "Induction" -> true
+      | IDENT "Minimality" -> false ] ]
+  ;
+  (* Various Binders *)
+  (* ... without coercions *)
+  simple_binder:
+    [ [ b = simple_binder_coe -> no_coercion loc b ] ]
+  ;
+  binder:
+    [ [ na = name ->  LocalRawAssum([na],CHole loc)
+      | "("; na = name; ")" -> LocalRawAssum([na],CHole loc)
+      | "("; na = name; ":"; c = lconstr; ")"
+          -> LocalRawAssum([na],c)
+      | "("; na = name; ":="; c = lconstr; ")" ->
+          LocalRawDef (na,c)
+    ] ]
+  ;
+  binder_nodef:
+    [ [ b = binder ->
+      (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 *)
+  local_decl_expr:
+    [ [ id = base_ident -> (false,AssumExpr(id,CHole loc))
+      | "("; id = base_ident; ")" -> (false,AssumExpr(id,CHole loc))
+      | "("; id = base_ident; oc = of_type_with_opt_coercion;
+             t = lconstr; ")" ->
+         (oc,AssumExpr (id,t))
+      | "("; id = base_ident; oc = of_type_with_opt_coercion;
+             t = lconstr; ":="; b = lconstr; ")" ->
+	 (oc,DefExpr (id,b,Some t))
+      | "("; id = base_ident; ":="; b = lconstr; ")" ->
+         match b with
+             CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
+           | _ -> (false,DefExpr(id,b,None)) ] ]
+  ;
+  simple_binder_coe:
+    [ [ id=base_ident -> (false,(id,CHole loc))
+      | "("; id = base_ident; ")" -> (false,(id,CHole loc))
+      | "("; id = base_ident; oc = of_type_with_opt_coercion;
+             t = lconstr; ")" ->
+         (oc,(id,t)) ] ]
+  ;
+  constructor_binder:
+    [ [ id = base_ident; coe = of_type_with_opt_coercion; c = lconstr ->
+        (coe,(id,c)) ] ]
+  ;
+  of_type_with_opt_coercion:
+    [ [ ":>" -> true
+      | ":"; ">" -> true
+      | ":" -> false ] ]
+  ;
+END
+
+
+(* Modules and Sections *)
+GEXTEND Gram
+  GLOBAL: gallina_ext module_expr module_type;
+
+  gallina_ext:
+    [ [ (* Interactive module declaration *)
+	IDENT "Module"; id = base_ident; 
+	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDefineModule (id, bl, mty_o, mexpr_o)
+	  
+      | IDENT "Module"; "Type"; id = base_ident; 
+	bl = LIST0 module_binder; mty_o = OPT is_module_type ->
+	  VernacDeclareModuleType (id, bl, mty_o)
+	  
+      | IDENT "Declare"; IDENT "Module"; id = base_ident; 
+	bl = LIST0 module_binder; mty_o = OPT of_module_type; 
+	mexpr_o = OPT is_module_expr ->
+	  VernacDeclareModule (id, bl, mty_o, mexpr_o)
+      (* Section beginning *)
+      | IDENT "Section"; id = base_ident -> VernacBeginSection id
+      | IDENT "Chapter"; id = base_ident -> VernacBeginSection id
+
+      (* This end a Section a Module or a Module Type *)
+      | IDENT "End"; id = base_ident -> 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 = STRING -> 
+	  VernacRequireFrom (export, specif, filename)
+      | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
+      | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ]
+  ;
+  export_token:
+    [ [ IDENT "Import" -> Some false
+      | IDENT "Export" -> Some true
+      | IDENT "Closed" -> None
+      |  -> Some false ] ]
+  ;
+  specif_token:
+    [ [ IDENT "Implementation" -> Some false
+      | IDENT "Specification" -> Some true
+      |  -> None ] ]
+  ;
+  of_module_type:
+    [ [ ":"; mty = module_type -> (mty, true) 
+      | "<:"; mty = module_type -> (mty, false) ] ]
+  ;
+  is_module_type:
+    [ [ ":="; mty = module_type -> mty ] ]
+  ;
+  is_module_expr:
+    [ [ ":="; mexpr = module_expr -> mexpr ] ]
+  ;
+
+  (* Module binder  *)
+  module_binder:
+    [ [ "("; id = base_ident; ":"; mty = module_type; ")" ->
+          ([id],mty) ] ]
+  ;
+
+  (* Module expressions *)
+  module_expr:
+    [ [ qid = qualid -> CMEident qid
+      | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2)
+      | "("; me = module_expr; ")" -> me
+(* ... *)
+      ] ]
+  ;
+  with_declaration:
+    [ [ IDENT "Definition"; id = base_ident; ":="; c = Constr.constr ->
+          CWith_Definition (id,c)
+      | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
+	  CWith_Module (id,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;
+
+  gallina_ext:
+    [ [ (* Transparent and Opaque *)
+        IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
+      | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l)
+
+      (* 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
+	  VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical)
+
+      (* Coercions *)
+      | IDENT "Coercion"; qid = global; d = def_body ->
+          let s = Ast.coerce_global_to_id qid in
+	  VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion)
+      | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
+           let s = Ast.coerce_global_to_id qid in
+	  VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion)
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
+         ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	   VernacIdentityCoercion (Local, f, s, t)
+      | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
+         s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	   VernacIdentityCoercion (Global, f, s, t)
+      | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
+	 s = class_rawexpr; ">->"; t = class_rawexpr -> 
+	  VernacCoercion (Local, qid, s, t)
+      | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
+         t = class_rawexpr ->
+	  VernacCoercion (Global, qid, s, t)
+
+      (* Implicit *)
+      | IDENT "Syntactic"; IDENT "Definition"; id = IDENT; ":="; c = lconstr;
+         n = OPT [ "|"; n = natural -> n ] ->
+	   let c = match n with
+	     | Some n ->
+		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
+		 CApp (loc,c,l)
+	     | None -> c in
+	   VernacNotation ("'"^id^"'",c,[],None,None)
+      | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
+	  VernacDeclareImplicits (qid,Some l)
+      | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
+
+      (* 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) ] ]
+  ;
+END
+
+GEXTEND Gram
+  GLOBAL: command check_command class_rawexpr;
+
+  command:
+    [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
+
+      (* System directory *)
+      | IDENT "Pwd" -> VernacChdir None
+      | IDENT "Cd" -> VernacChdir None
+      | IDENT "Cd"; dir = 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 = STRING -> s | s = IDENT -> s ] ->
+	  VernacLoad (verbosely, s)
+      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
+	  VernacDeclareMLModule l
+
+      (* Dump of the universe graph - to file or to stdout *) 
+      | IDENT "Dump"; IDENT "Universes"; fopt = OPT STRING ->
+	  VernacPrint (PrintUniverses fopt)
+
+      | IDENT "Locate"; l = locatable -> VernacLocate l
+
+      (* Managing load paths *)
+      | IDENT "Add"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath ->
+	  VernacAddLoadPath (false, dir, alias)
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = STRING; 
+	  alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
+      | IDENT "Remove"; IDENT "LoadPath"; dir = STRING ->
+	  VernacRemoveLoadPath dir
+
+       (* For compatibility *)
+      | IDENT "AddPath"; dir = STRING; "as"; alias = as_dirpath ->
+	  VernacAddLoadPath (false, dir, alias)
+      | IDENT "AddRecPath"; dir = STRING; "as"; alias = as_dirpath ->
+	  VernacAddLoadPath (true, dir, alias)
+      | IDENT "DelPath"; dir = 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" -> VernacPrint PrintLocalContext 
+      | 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)
+
+      (* 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"; qid = global; l = in_or_out_modules -> 
+	  VernacSearch (SearchAbout qid, l)
+
+      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
+	  VernacAddMLPath (false, dir)
+      | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = 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) ] ]
+  ;
+  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"; uni = IDENT; ent = IDENT ->
+          (* This should be in "syntax" section but is here for factorization*)
+	  PrintGrammar (uni, ent)
+      | IDENT "LoadPath" -> PrintLoadPath
+      | IDENT "Modules" -> PrintModules
+
+      | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath
+      | IDENT "ML"; IDENT "Modules" -> PrintMLModules
+      | IDENT "Graph" -> PrintGraph
+      | IDENT "Classes" ->  PrintClasses
+      | IDENT "Coercions" -> PrintCoercions
+      | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
+         -> PrintCoercionPaths (s,t)
+      | IDENT "Tables" -> PrintTables
+      | IDENT "Proof"; qid = global -> PrintOpaqueName qid
+      | IDENT "Hint" -> PrintHintGoal
+      | IDENT "Hint"; qid = global -> PrintHint qid
+      | IDENT "Hint"; "*" -> PrintHintDb
+      | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
+      | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
+  ;
+  class_rawexpr:
+    [ [ IDENT "FUNCLASS" -> FunClass
+      | IDENT "SORTCLASS" -> SortClass
+      | qid = global -> RefClass qid ] ]
+  ;
+  locatable:
+    [ [ qid = global -> LocateTerm qid
+      | IDENT "File"; f = STRING -> LocateFile f
+      | IDENT "Library"; qid = global -> LocateLibrary  qid
+      | s = 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 "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s
+      | IDENT "Restore"; IDENT "State"; s = 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
+
+(* Tactic Debugger *)
+      |	IDENT "Debug"; IDENT "On" -> VernacDebug true
+      |	IDENT "Debug"; IDENT "Off" -> VernacDebug false
+
+ ] ];
+    END
+;;
+
+(* Grammar extensions *)
+	  
+GEXTEND Gram
+  GLOBAL: syntax;
+
+  syntax:
+   [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
+
+     | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
+	 VernacDelimiters (sc,key)
+
+     | IDENT "Arguments"; IDENT "Scope"; qid = global;
+         "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
+
+     | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING; 
+         p = global;
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
+         let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in
+         VernacInfix (a,n,op,p,b,None,sc)
+     | IDENT "Notation"; s = IDENT; ":="; c = constr ->
+	 VernacNotation ("'"^s^"'",c,[],None,None)
+     | IDENT "Notation"; s = STRING; ":="; c = constr;
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
+           VernacNotation (s,c,modl,None,sc)
+
+     | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
+        OPT [ ":"; IDENT "tactic" ]; ":=";
+        OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> 
+	  VernacTacticGrammar tl
+
+     | IDENT "Grammar"; u = univ;
+         tl = LIST1 grammar_entry SEP "with" -> 
+	   VernacGrammar (rename_command_entry u,tl)
+
+     | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP "," ->
+         VernacSyntax (u,el)
+
+     | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING; 
+	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
+	 -> VernacSyntaxExtension (s,l)
+
+     (* "Print" "Grammar" should be here but is in "command" entry in order 
+        to factorize with other "Print"-based vernac entries *)
+  ] ]
+  ;
+  univ:
+  [ [ univ = IDENT ->
+        set_default_action_parser (parser_type_from_name univ); univ ] ]
+  ;
+  syntax_modifier:
+    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
+        SetItemLevel ([x],n)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level";
+        n = natural -> SetItemLevel (x::l,n)
+      | IDENT "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 ] ]
+  ;
+  syntax_extension_type:
+    [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
+      | IDENT "bigint" -> ETBigint
+      | e=IDENT -> ETOther("constr",e)
+    ] ]
+  ;
+  opt_scope:
+    [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ]
+  ;
+  (* Syntax entries for Grammar. Only grammar_entry is exported *)
+  grammar_entry:
+    [[ nont = IDENT; set_entry_type; ":=";
+       ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
+	 (rename_command_entry nont,ep,rl) ]]
+  ;
+  entry_prec:
+    [[ IDENT "LEFTA" -> Some Gramext.LeftA
+     | IDENT "RIGHTA" -> Some Gramext.RightA
+     | IDENT "NONA" -> Some Gramext.NonA
+     | -> None ]]
+  ;
+  grammar_tactic_rule:
+    [[ name = rule_name; "["; s = STRING; pil = LIST0 production_item; "]";
+       "->"; "["; t = Tactic.tactic; "]"  -> (name, (s,pil), t) ]]
+  ;
+  grammar_rule:
+    [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
+       a = action -> (name, pil, a) ]]
+  ;
+  rule_name:
+    [[ name = IDENT -> name ]]
+  ;
+  production_item:
+    [[ s = STRING -> VTerm s
+     | nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] ->
+         match po with
+           | Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p))
+           | _ -> VNonTerm (loc,nt,None) ]]
+  ;
+  non_terminal:
+    [[ u = IDENT; ":"; nt = IDENT ->
+        NtQual(rename_command_entry u, rename_command_entry nt)
+     | nt = IDENT -> NtShort (rename_command_entry nt) ]]
+  ;
+
+
+  (* Syntax entries for Syntax. Only syntax_entry is exported *)
+  syntax_entry:
+    [ [ IDENT "level"; p = precedence; ":";
+	OPT "|"; rl = LIST1 syntax_rule SEP "|" -> (p,rl) ] ]
+  ;
+  syntax_rule:
+    [ [ nm = IDENT; "["; s = astpat; "]"; "->"; u = unparsing -> (nm,s,u) ] ]
+  ;
+  precedence:
+    [ [ a = natural -> a
+(*      | "["; a1 = natural; a2 = natural; a3 = natural; "]" -> (a1,a2,a3)*)
+    ] ]
+  ;
+  unparsing:
+    [ [ "["; ll = LIST0 next_hunks; "]" -> ll ] ]
+  ;
+  next_hunks:
+    [ [ IDENT "FNL" -> UNP_FNL
+      | IDENT "TAB" -> UNP_TAB
+      | c = STRING -> RO c
+      | "[";
+        x =
+          [ b = box; ll = LIST0 next_hunks -> UNP_BOX (b,ll)
+          | n = natural; m = natural -> UNP_BRK (n, m)
+          | IDENT "TBRK"; n = natural; m = natural -> UNP_TBRK (n, m) ];
+        "]" -> x
+      | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] ->
+          match oprec with
+	    | Some (ext,pr) -> PH (e,ext,pr)
+            | None -> PH (e,None,Any)
+ ]]
+  ;
+  box:
+    [ [ "<"; bk = box_kind; ">" -> bk ] ]
+  ;
+  box_kind:
+    [ [ IDENT "h"; n = natural -> PpHB n
+      | IDENT "v"; n = natural -> PpVB n
+      | IDENT "hv"; n = natural -> PpHVB n
+      | IDENT "hov"; n = natural -> PpHOVB n
+      | IDENT "t" -> PpTB ] ]
+  ;
+  paren_reln_or_extern:
+    [ [ IDENT "L" -> None, L
+      | IDENT "E" -> None, E
+      | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
+	  match precrec with
+	    | Some p -> Some pprim, Prec p
+            | None -> Some pprim, Any ] ]
+  ;
+  (* meta-syntax entries *)
+  astpat:
+    [ [ "<<" ; a = Prim.ast; ">>" -> a 
+      | a = Constr.lconstr -> 
+	  Termast.ast_of_rawconstr 
+	  (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
+    ] ]
+  ; 
+  action:
+    [ [ IDENT "let"; p = Prim.astlist; et = set_internal_entry_type;
+        "="; e1 = action; "in"; e = action -> Ast.CaseAction (loc,e1,et,[p,e])
+      | IDENT "case"; a = action; et = set_internal_entry_type; "of";
+        cl = LIST1 case SEP "|"; IDENT "esac" -> Ast.CaseAction (loc,a,et,cl)
+      | "["; a = default_action_parser; "]" -> Ast.SimpleAction (loc,a) ] ]
+  ;
+  case:
+    [[ p = Prim.astlist; "->"; a = action -> (p,a) ]]
+  ;
+  set_internal_entry_type:
+    [[ ":"; IDENT "ast"; IDENT "list" -> Ast.ETastl
+     | [ ":"; IDENT "ast" -> () | -> () ] -> Ast.ETast ]]
+  ;
+  set_entry_type:
+    [[ ":"; et = entry_type -> set_default_action_parser et
+     | -> () ]]
+  ;
+  entry_type:
+    [[ IDENT "ast"; IDENT "list" -> Util.error "type ast list no longer supported"
+     | IDENT "ast" -> Util.error "type ast no longer supported"
+     | IDENT "constr" -> ConstrParser
+     | IDENT "pattern" -> CasesPatternParser
+     | IDENT "tactic" -> assert false
+     | IDENT "vernac" -> Util.error "vernac extensions no longer supported" ] ]
+  ;
+END
+
+(* Reinstall tactic and vernac extensions *)
+let _ = Egrammar.reset_extend_grammars_v8()
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 5103aedb0..11c88d113 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -54,11 +54,15 @@ let z_of_string pos_or_neg s dloc =
     aZERO
 
 (* Declare the primitive parser with Grammar and without the scope mechanism *)
-open Pcoq
+let zsyntax_create name =
+  let e =
+    Pcoq.create_constr_entry (Pcoq.get_univ "znatural") name in
+  Pcoq.Gram.Unsafe.clear_entry e;
+  e
 
-let number = create_constr_entry (get_univ "znatural") "number" 
+let number = zsyntax_create "number" 
 
-let negnumber = create_constr_entry (get_univ "znatural") "negnumber"
+let negnumber = zsyntax_create "negnumber"
  
 let _ =
   Gram.extend number None
diff --git a/parsing/g_zsyntaxnew.ml b/parsing/g_zsyntaxnew.ml
new file mode 100644
index 000000000..24b6d4137
--- /dev/null
+++ b/parsing/g_zsyntaxnew.ml
@@ -0,0 +1,168 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Coqast
+open Pcoq
+open Pp
+open Util
+open Names
+open Ast
+open Extend
+open Topconstr
+open Libnames
+open Bignat
+
+(**********************************************************************)
+(* Parsing positive via scopes                                        *)
+(**********************************************************************)
+
+open Libnames
+open Rawterm
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let fast_integer_module = make_dir ["Coq";"ZArith";"fast_integer"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let positive_path = make_path fast_integer_module (id_of_string "positive")
+let path_of_xI = ((positive_path,0),1)
+let path_of_xO = ((positive_path,0),2)
+let path_of_xH = ((positive_path,0),3)
+let glob_xI = ConstructRef path_of_xI
+let glob_xO = ConstructRef path_of_xO
+let glob_xH = ConstructRef path_of_xH
+
+let pos_of_bignat dloc x =
+  let ref_xI = RRef (dloc, glob_xI) in
+  let ref_xH = RRef (dloc, glob_xH) in
+  let ref_xO = RRef (dloc, glob_xO) in
+  let rec pos_of x =
+    match div2_with_rest x with
+      | (q,false) -> RApp (dloc, ref_xO,[pos_of q])
+      | (q,true) when is_nonzero q -> RApp (dloc,ref_xI,[pos_of q])
+      | (q,true) -> ref_xH
+  in 
+  pos_of x
+
+let interp_positive dloc = function
+  | POS n when is_nonzero n -> pos_of_bignat dloc n
+  | _ ->
+      user_err_loc (dloc, "interp_positive",
+        str "Only strictly positive numbers in type \"positive\"!")
+
+let rec pat_pos_of_bignat dloc x name =
+  match div2_with_rest x with
+    | (q,false) -> 
+        PatCstr (dloc,path_of_xO,[pat_pos_of_bignat dloc q Anonymous],name)
+    | (q,true) when is_nonzero q -> 
+        PatCstr (dloc,path_of_xI,[pat_pos_of_bignat dloc q Anonymous],name)
+    | (q,true) ->
+        PatCstr (dloc,path_of_xH,[],name)
+
+let pat_interp_positive dloc = function
+  | POS n -> pat_pos_of_bignat dloc n
+  | NEG n ->
+      user_err_loc (dloc, "interp_positive",
+        str "No negative number in type \"positive\"!")
+
+(**********************************************************************)
+(* Printing positive via scopes                                       *)
+(**********************************************************************)
+
+exception Non_closed_number
+
+let rec bignat_of_pos = function
+  | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
+  | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | RRef (_, a) when a = glob_xH -> Bignat.one
+  | _ -> raise Non_closed_number
+
+let uninterp_positive p =
+  try 
+    Some (POS (bignat_of_pos p))
+  with Non_closed_number -> 
+    None
+
+(***********************************************************************)
+(* Declaring interpreters and uninterpreters for positive *)
+(***********************************************************************)
+
+let _ = Symbols.declare_numeral_interpreter "positive_scope"
+  ["Coq";"ZArith";"Zsyntax"]
+  (interp_positive,Some pat_interp_positive)
+  ([RRef (dummy_loc, glob_xI); 
+    RRef (dummy_loc, glob_xO); 
+    RRef (dummy_loc, glob_xH)],
+   uninterp_positive,
+   None)
+
+(**********************************************************************)
+(* Parsing Z via scopes                                               *)
+(**********************************************************************)
+
+let z_path = make_path fast_integer_module (id_of_string "Z")
+let glob_z = IndRef (z_path,0)
+let path_of_ZERO = ((z_path,0),1)
+let path_of_POS = ((z_path,0),2)
+let path_of_NEG = ((z_path,0),3)
+let glob_ZERO = ConstructRef path_of_ZERO
+let glob_POS = ConstructRef path_of_POS
+let glob_NEG = ConstructRef path_of_NEG
+
+let z_of_posint dloc pos_or_neg n = 
+  if is_nonzero n then
+    let sgn = if pos_or_neg then glob_POS else glob_NEG in
+    RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
+  else 
+    RRef (dloc, glob_ZERO)
+
+let z_of_int dloc z =
+  match z with
+  | POS n -> z_of_posint dloc true n 
+  | NEG n -> z_of_posint dloc false n 
+
+let pat_z_of_posint dloc pos_or_neg n name = 
+  if is_nonzero n then
+    let sgn = if pos_or_neg then path_of_POS else path_of_NEG in
+    PatCstr (dloc, sgn, [pat_pos_of_bignat dloc n Anonymous], name)
+  else 
+    PatCstr (dloc, path_of_ZERO, [], name)
+
+let pat_z_of_int dloc n name =
+  match n with
+  | POS n -> pat_z_of_posint dloc true n name
+  | NEG n -> pat_z_of_posint dloc false n name
+
+(**********************************************************************)
+(* Printing Z via scopes                                              *)
+(**********************************************************************)
+
+let bigint_of_z = function
+  | RApp (_, RRef (_,b),[a]) when b = glob_POS -> POS (bignat_of_pos a)
+  | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> NEG (bignat_of_pos a)
+  | RRef (_, a) when a = glob_ZERO -> POS (Bignat.zero)
+  | _ -> raise Non_closed_number
+
+let uninterp_z p =
+  try
+    Some (bigint_of_z p)
+  with Non_closed_number -> None
+
+(***********************************************************************)
+(* Declaring interpreters and uninterpreters for Z *)
+
+let _ = Symbols.declare_numeral_interpreter "Z_scope"
+  ["Coq";"ZArith";"Zsyntax"]
+  (z_of_int,Some pat_z_of_int)
+  ([RRef (dummy_loc, glob_ZERO); 
+    RRef (dummy_loc, glob_POS); 
+    RRef (dummy_loc, glob_NEG)],
+  uninterp_z,
+  None)
diff --git a/parsing/g_zsyntaxnew.mli b/parsing/g_zsyntaxnew.mli
new file mode 100644
index 000000000..a8370f630
--- /dev/null
+++ b/parsing/g_zsyntaxnew.mli
@@ -0,0 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(* Nice syntax for integers. *)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index ff54f74ef..54d0c42c0 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -151,22 +151,7 @@ let unfreeze (kw,tt) =
   token_tree := tt
 
 let init () =
-  unfreeze (empty_ttree, empty_ttree);
-  List.iter add_keyword
-    [ "Grammar"; "Syntax"; "Quit"; "Load"; "Compile";
-      "of"; "with"; "end"; "as"; "in"; "using";
-      "Cases"; "Fixpoint"; "CoFixpoint";
-      "Definition"; "Inductive"; "CoInductive"; 
-      "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
-      "Orelse"; "Proof"; "Qed";
-      "Prop"; "Set"; "Type"; "And"
-    ]; (* "let" is not a keyword because #Core#let.cci would not parse *)
-  List.iter add_special_token 
-    [ ":"; "("; ")"; "["; "]"; "{"; "}"; "_"; ";"; "`"; "``"; 
-      "()"; "->"; "\\/"; "/\\"; "|-"; ":="; "<->"; "!"; "$"; "%"; "&";
-      "*"; "+"; ","; "@"; "^"; "#"; "\\"; "/"; "-"; "<"; ">"; 
-      "|"; "?"; "="; "~"; "'"; "<<"; ">>"; "<>"; "::";
-      "<:"; ":<"; "=>"; ">->" ]
+  unfreeze (empty_ttree, empty_ttree)
 
 let _ = init()
 
@@ -318,20 +303,11 @@ let parse_226_tail tk = parser
   | [< len = ident (store 0 '\226') >] ->
       TokIdent (get_buff len)
 
-(* Parse a token in a char stream *)
 
-let rec next_token = parser bp
-  | [< ''\n'; s >] -> (match !current with
-	| BeVernac s -> current := InComment s
-	| InComment _ -> add_comment_pp (fnl ())
-	| _ -> ()); next_token s
-  | [< '' ' | '\t'; s >] -> (match !current with
-	| BeVernac _ |  InComment _ -> add_comment_pp (spc ())
-	| _ -> ()); next_token s
-  | [< ''\r'; s >] -> next_token s
-  | [< ''$'; len = ident (store 0 '$') >] ep -> 
-      (("METAIDENT", get_buff len), (bp,ep))
-  | [< ''.' as c; t = parser
+(* Parse what foolows a dot *)
+let parse_after_dot bp c strm =
+  if !Options.v7 then 
+    match strm with parser
 	 | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
 	     ("FIELD", get_buff len)
 	 (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
@@ -349,10 +325,26 @@ let rec next_token = parser bp
 	 | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c);
 	   len = ident (store 0 c) >] ->
 	     ("FIELD", get_buff len)
-(*
-	 | [< >] -> ("", ".") >] ep -> (t, (bp,ep))
-*)
-	 | [< (t,_) = process_chars bp c >] -> t >] ep ->
+	 | [< (t,_) = process_chars bp c >] -> t
+  else
+    match strm with parser
+	 | [< (t,_) = process_chars bp c >] -> t
+
+
+(* Parse a token in a char stream *)
+
+let rec next_token = parser bp
+  | [< ''\n'; s >] -> (match !current with
+	| BeVernac s -> current := InComment s
+	| InComment _ -> add_comment_pp (fnl ())
+	| _ -> ()); next_token s
+  | [< '' ' | '\t'; s >] -> (match !current with
+	| BeVernac _ |  InComment _ -> add_comment_pp (spc ())
+	| _ -> ()); next_token s
+  | [< ''\r'; s >] -> next_token s
+  | [< ''$'; len = ident (store 0 '$') >] ep -> 
+      (("METAIDENT", get_buff len), (bp,ep))
+  | [< ''.' as c; t = parse_after_dot bp c >] ep ->
       current:=BeVernac ""; (t, (bp,ep))
   | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
       let id = get_buff len in current:=InVernac; 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 33948d83b..6cff40c34 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -344,7 +344,7 @@ module Constr =
 
     (* Entries that can be refered via the string -> Gram.Entry.e table *)
     let constr = gec_constr "constr"
-    let constr9 = gec_constr "constr9"
+    let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
     let lconstr = gec_constr "lconstr"
     let ident = make_gen_entry uconstr rawwit_ident "ident"
@@ -398,14 +398,36 @@ module Vernac_ =
     let syntax = gec_vernac "syntax_command"
     let vernac = gec_vernac "Vernac_.vernac"
 
-    (* Various vernacular entries needed to be exported *)
-    let thm_token = Gram.Entry.create "vernac:thm_token"
-    let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
-
     let vernac_eoi = eoi_entry vernac
   end
 
 
+(* Prim is not re-initialized *)
+let reset_all_grammars () =
+  let f = Gram.Unsafe.clear_entry in
+  List.iter f
+    [Constr.constr;Constr.operconstr;Constr.lconstr;Constr.annot;
+     Constr.constr_pattern];
+  f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern;
+  f Module.module_expr; f Module.module_type;
+  f Tactic.simple_tactic;
+  f Tactic.castedopenconstr;
+  f Tactic.constr_with_bindings;
+  f Tactic.constrarg;
+  f Tactic.quantified_hypothesis;
+  f Tactic.int_or_var;
+  f Tactic.red_expr;
+  f Tactic.tactic_arg;
+  f Tactic.tactic;
+  f Vernac_.gallina;
+  f Vernac_.gallina_ext;
+  f Vernac_.command;
+  f Vernac_.syntax;
+  f Vernac_.vernac;
+  Lexer.init()
+
+
+
 let main_entry = Gram.Entry.create "vernac"
 
 GEXTEND Gram
@@ -425,8 +447,6 @@ open Vernac_
 let globalizer = ref (fun x -> failwith "No globalizer")
 let set_globalizer f = globalizer := f
 
-let f = (ast : Coqast.t G.Entry.e)
-
 let define_ast_quotation default s (e:Coqast.t G.Entry.e) =
   (if default then
     GEXTEND Gram
@@ -462,7 +482,7 @@ GEXTEND Gram
   dynconstr:
   [ [ a = Constr.constr -> ConstrNode a 
     (* For compatibility *)
-    | "<<"; a = Constr.constr; ">>" -> ConstrNode a ] ]
+    | "<<"; a = Constr.lconstr; ">>" -> ConstrNode a ] ]
   ;
   dyncasespattern: [ [ a = Constr.pattern -> CasesPatternNode a ] ];
 END
@@ -527,9 +547,7 @@ let adjust_level assoc from = function
 	| _ -> Some (Some n)
 
 let compute_entry allow_create adjust = function
-  | ETConstr (10,_) -> weaken_entry Constr.lconstr, None, true
-  | ETConstr (9,_) -> weaken_entry Constr.constr9, None, true
-  | ETConstr (n,q) -> weaken_entry Constr.constr, adjust (n,q), false
+  | ETConstr (n,q) -> weaken_entry Constr.operconstr, adjust (n,q), false
   | ETIdent -> weaken_entry Constr.ident, None, false
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
@@ -543,19 +561,50 @@ let compute_entry allow_create adjust = function
         with e when allow_create -> create_entry u n ConstrArgType in
       object_of_typed_entry e, None, true
 
-let get_constr_entry = compute_entry true (fun (n,()) -> Some n)
-
-let get_constr_production_entry ass from =
-  compute_entry false (adjust_level ass from)
+let get_constr_entry en =
+  match en with
+      ETConstr(200,_) when not !Options.v7 ->
+        snd (get_entry (get_univ "constr") "binder_constr"),
+        None,
+        false
+    | _ -> compute_entry true (fun (n,()) -> Some n) en
+
+let get_constr_production_entry ass from en =
+  (* first 2 cases to help factorisation *)
+  match en with
+    | ETConstr (10,q) when !Options.v7 ->
+        weaken_entry Constr.lconstr, None, false
+    | ETConstr (8,q) when !Options.v7 ->
+        weaken_entry Constr.constr, None, false
+    | _ -> compute_entry false (adjust_level ass from) en
 
 let constr_prod_level = function
-  | 8 -> "top"
-  | 4 -> "4L"
+  | 4 when !Options.v7 -> "4L"
   | n -> string_of_int n
 
+let is_self from e =
+  match from, e with
+      ETConstr(n,_), ETConstr(n',
+        BorderProd(false,Some(Gramext.NonA|Gramext.LeftA))) -> false
+    | ETConstr(n,_), ETConstr(n',_) -> n=n'
+    | (ETIdent,ETIdent | ETReference, ETReference | ETBigint,ETBigint
+      | ETPattern, ETPattern) -> true
+    | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2'
+    | _ -> false
+
+let is_binder_level from e =
+  match from, e with
+      ETConstr(200,_), ETConstr(200,_) -> not !Options.v7
+    | _ -> false
+
 let symbol_of_production assoc from typ =
-  match get_constr_production_entry assoc from typ with
-    | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
-    | (eobj,Some None,_) -> Gramext.Snext
-    | (eobj,Some (Some lev),_) -> 
-        Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)
+  if is_binder_level from typ then
+    let eobj = snd (get_entry (get_univ "constr") "operconstr") in
+    Gramext.Snterml (Gram.Entry.obj eobj,"200")
+  else if is_self from typ then Gramext.Sself
+  else
+    match get_constr_production_entry assoc from typ with
+      | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
+      | (eobj,Some None,_) -> Gramext.Snext
+      | (eobj,Some (Some lev),_) -> 
+          Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b15046c29..325d4f494 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -129,9 +129,9 @@ module Prim :
 module Constr :
   sig
     val constr : constr_expr Gram.Entry.e
-    val constr9 : constr_expr Gram.Entry.e
     val constr_eoi : constr_expr Gram.Entry.e
     val lconstr : constr_expr Gram.Entry.e
+    val operconstr : constr_expr Gram.Entry.e
     val ident : identifier Gram.Entry.e
     val global : reference Gram.Entry.e
     val sort : rawsort Gram.Entry.e
@@ -164,8 +164,6 @@ module Tactic :
 module Vernac_ :
   sig
     open Decl_kinds
-    val thm_token : theorem_kind Gram.Entry.e
-    val class_rawexpr : class_rawexpr Gram.Entry.e
     val gallina : vernac_expr Gram.Entry.e
     val gallina_ext : vernac_expr Gram.Entry.e
     val command : vernac_expr Gram.Entry.e
@@ -173,3 +171,5 @@ module Vernac_ :
     val vernac : vernac_expr Gram.Entry.e
     val vernac_eoi : vernac_expr Gram.Entry.e
   end
+
+val reset_all_grammars : unit -> unit
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 57e813632..97c7d637b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -22,55 +22,6 @@ open Topconstr
 open Term
 (*i*)
 
-let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
-
-let pr_global ref = pr_global_env None ref
-
-let global_const_name kn =
-  try pr_global (ConstRef kn)
-  with Not_found -> (* May happen in debug *)
-    (str ("CONST("^(string_of_kn kn)^")"))
-
-let global_var_name id =
-  try pr_global (VarRef id)
-  with Not_found -> (* May happen in debug *)
-    (str ("SECVAR("^(string_of_id id)^")"))
-
-let global_ind_name (kn,tyi) =
-  try pr_global (IndRef (kn,tyi))
-  with Not_found -> (* May happen in debug *)
-    (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
-
-let global_constr_name ((kn,tyi),i) =
-  try pr_global (ConstructRef ((kn,tyi),i))
-  with Not_found -> (* May happen in debug *)
-    (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
-		  ^","^(string_of_int i)^")"))
-
-let globpr gt = match gt with
-  | Nvar(_,s) -> (pr_id s)
-  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
-  | Node(_,"CONST",[Path(_,sl)]) ->
-      global_const_name (section_path sl)
-  | Node(_,"SECVAR",[Nvar(_,s)]) ->
-      global_var_name s
-  | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
-      global_ind_name (section_path sl, tyi)
-  | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
-      global_constr_name ((section_path sl, tyi), i)
-  | Dynamic(_,d) ->
-    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
-    else dfltpr gt
-  | gt -> dfltpr gt
-
-let wrap_exception = function
-    Anomaly (s1,s2) ->
-      warning ("Anomaly ("^s1^")"); pp s2;
-      str"<PP error: non-printable term>"
-  | Failure _ | UserError _ | Not_found ->
-      str"<PP error: non-printable term>"
-  | s -> raise s
-
 let latom = 0
 let lannot = 1
 let lprod = 8 (* not 1 because the scope extends to 8 on the right *)
@@ -157,6 +108,8 @@ let pr_binder pr (nal,t) =
 let pr_binders pr bl =
   hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
 
+let pr_global vars ref = pr_global_env vars ref
+
 let rec pr_lambda_tail pr bll = function
   | CLambdaN (_,bl,a) ->
       pr_lambda_tail pr (bll ++ pr_semicolon() ++ pr_binders pr bl) a
@@ -230,21 +183,22 @@ let pr_annotation pr = function
   | None -> mt ()
   | Some t -> str "<" ++ pr ltop t ++ str ">" ++ brk (0,2)
 
-let rec pr_pat = function
-  | CPatAlias (_,p,x) -> pr_pat p ++ spc () ++ str "as" ++ spc () ++ pr_id x
+let rec pr_cases_pattern = function
+  | CPatAlias (_,p,x) ->
+      pr_cases_pattern p ++ spc () ++ str "as" ++ spc () ++ pr_id x
   | CPatCstr (_,c,[]) -> pr_reference c
   | CPatCstr (_,c,pl) ->
       hov 0 (
 	str "(" ++ pr_reference c ++ spc () ++ 
-	prlist_with_sep spc pr_pat pl ++ str ")")
+	prlist_with_sep spc pr_cases_pattern pl ++ str ")")
   | CPatAtom (_,Some c) -> pr_reference c
   | CPatAtom (_,None) -> str "_"
   | CPatNumeral (_,n) -> Bignat.pr_bigint n
-  | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_pat p)
+  | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_cases_pattern p)
 
 let pr_eqn pr (_,patl,rhs) =
   hov 0 (
-    prlist_with_sep spc pr_pat patl ++ spc () ++
+    prlist_with_sep spc pr_cases_pattern patl ++ spc () ++
     str "=>" ++
     brk (1,1) ++ pr ltop rhs) ++ spc ()
 
@@ -394,26 +348,3 @@ let rec pr_may_eval pr = function
 	 str "[" ++ pr c ++ str "]")
   | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c)
   | ConstrTerm c -> pr c
-
-(**********************************************************************)
-let constr_syntax_universe = "constr"
-(* This is starting precedence for printing constructions or tactics *)
-(* Level 9 means no parentheses except for applicative terms (at level 10) *)
-let constr_initial_prec = Some (9,Ppextend.L)
-
-let gentermpr_fail gt =
-  Esyntax.genprint globpr constr_syntax_universe constr_initial_prec gt
-
-let gentermpr gt =
-  try gentermpr_fail gt
-  with s -> wrap_exception s
-
-(* [at_top] means ids of env must be avoided in bound variables *)
-
-let gentermpr_core at_top env t =
-  gentermpr (Termast.ast_of_constr at_top env t)
-(*
-let gentermpr_core at_top env t =
-  pr_constr (Constrextern.extern_constr at_top env t)
-*)
-  
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1a2848f00..6dd3d842c 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -23,10 +23,7 @@ open Util
 val split_fix : int -> constr_expr -> constr_expr -> 
   (name located list * constr_expr) list * constr_expr * constr_expr
 
-val pr_global : global_reference -> std_ppcmds
-
-val gentermpr : Coqast.t -> std_ppcmds
-val gentermpr_core : bool -> env -> constr -> std_ppcmds
+val pr_global : Idset.t -> global_reference -> std_ppcmds
 
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val pr_name : name -> std_ppcmds
@@ -39,4 +36,5 @@ val pr_occurrences : ('a -> std_ppcmds) -> 'a occurrences -> std_ppcmds
 val pr_sort : rawsort -> std_ppcmds
 val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds
 val pr_constr : constr_expr -> std_ppcmds
+val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2f18076b7..fbeb697eb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -13,22 +13,32 @@ open Names
 open Nameops
 open Util
 open Extend
-open Ppconstr
 open Tacexpr
 open Rawterm
 open Topconstr
 open Genarg
 open Libnames
 
+let pr_red_expr = Ppconstr.pr_red_expr
+let pr_may_eval = Ppconstr.pr_may_eval
+let pr_sort = Ppconstr.pr_sort
+let pr_global = Ppconstr.pr_global Idset.empty
+let pr_name = Ppconstr.pr_name
+let pr_opt = Ppconstr.pr_opt
+let pr_occurrences = Ppconstr.pr_occurrences
+
   (* Extensions *)
+let prtac_tab_v7 = Hashtbl.create 17
 let prtac_tab = Hashtbl.create 17
 
-let declare_extra_tactic_pprule s f g =
-  Hashtbl.add prtac_tab s (f,g)
+let declare_extra_tactic_pprule for_v8 s f g =
+  Hashtbl.add prtac_tab_v7 s (f,g);
+  if for_v8 then Hashtbl.add prtac_tab s (f,g)
 
+let genarg_pprule_v7 = ref Stringmap.empty
 let genarg_pprule = ref Stringmap.empty
 
-let declare_extra_genarg_pprule (rawwit, f) (wit, g) =
+let declare_extra_genarg_pprule for_v8 (rawwit, f) (wit, g) =
   let s = match unquote wit with
     | ExtraArgType s -> s 
     | _ -> error
@@ -36,7 +46,9 @@ let declare_extra_genarg_pprule (rawwit, f) (wit, g) =
   in
   let f x = f (out_gen rawwit x) in
   let g x = g (out_gen wit x) in
-  genarg_pprule := Stringmap.add s (f,g) !genarg_pprule 
+  genarg_pprule_v7 := Stringmap.add s (f,g) !genarg_pprule_v7;
+  if for_v8 then
+    genarg_pprule := Stringmap.add s (f,g) !genarg_pprule 
 
 (* [pr_rawtac] is here to cheat with ML typing system,
    gen_tactic_expr is polymorphic but with some occurrences of its
@@ -66,8 +78,6 @@ let pr_or_meta pr = function
   | AI x -> pr x
   | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable"
 
-let pr_casted_open_constr = pr_constr
-
 let pr_quantified_hypothesis = function
   | AnonHyp n -> int n
   | NamedHyp id -> pr_id id 
@@ -133,9 +143,9 @@ let pr_induction_arg prc = function
   | ElimOnAnonHyp n -> int n
 
 let pr_match_pattern = function
-  | Term a -> pr_pattern a
-  | Subterm (None,a) -> str "[" ++ pr_pattern a ++ str "]"
-  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pattern a ++ str "]"
+  | Term a -> Ppconstr.pr_pattern a
+  | Subterm (None,a) -> str "[" ++ Ppconstr.pr_pattern a ++ str "]"
+  | Subterm (Some id,a) -> pr_id id ++ str "[" ++ Ppconstr.pr_pattern a ++ str "]"
 
 let pr_match_hyps = function
   | NoHypId mp -> str "_:" ++ pr_match_pattern mp
@@ -146,7 +156,8 @@ let pr_match_rule m pr = function
       str "[" ++ pr_match_pattern mp ++ str "]"
       ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
   | Pat (rl,mp,t) ->
-      str "[" ++ prlist_with_sep pr_semicolon pr_match_hyps rl ++ spc () ++ 
+      str "[" ++ prlist_with_sep pr_semicolon
+                   pr_match_hyps rl ++ spc () ++ 
       str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++
       spc () ++ str "->" ++ brk (1,2) ++ pr t
   | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t
@@ -192,7 +203,16 @@ let pr_autoarg_usingTDB = function
   | true -> spc () ++ str "Using TDB"
   | false -> mt ()
 
-let rec pr_rawgen prtac x =
+let rec pr_tacarg_using_rule pr_gen = function
+  | Egrammar.TacTerm s :: l, al ->
+      spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al)
+  | Egrammar.TacNonTerm _ :: l, a :: al ->
+      pr_gen a ++ pr_tacarg_using_rule  pr_gen (l,al)
+  | [], [] -> mt ()
+  | _ -> failwith "Inconsistent arguments of extended tactic"
+
+
+let rec pr_rawgen prc prtac x =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
   | IntArgType -> pr_arg int (out_gen rawwit_int x)
@@ -202,45 +222,44 @@ let rec pr_rawgen prtac x =
   | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x)
   | RefArgType -> pr_arg pr_reference (out_gen rawwit_ref x)
   | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x)
-  | ConstrArgType -> pr_arg pr_constr (out_gen rawwit_constr x)
+  | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_arg (pr_may_eval pr_constr) (out_gen rawwit_constr_may_eval x)
+      pr_arg (pr_may_eval prc) (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
-      pr_arg (pr_red_expr (pr_constr,pr_metanum pr_reference)) (out_gen rawwit_red_expr x)
+      pr_arg (pr_red_expr (prc,pr_metanum pr_reference)) (out_gen rawwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
   | CastedOpenConstrArgType ->
-      pr_arg pr_casted_open_constr (out_gen rawwit_casted_open_constr x)
+      pr_arg prc (out_gen rawwit_casted_open_constr x)
   | ConstrWithBindingsArgType -> 
-      pr_arg (pr_with_bindings pr_constr)
+      pr_arg (pr_with_bindings prc)
       (out_gen rawwit_constr_with_bindings x)
   | List0ArgType _ -> 
-      hov 0 (fold_list0 (fun x a -> pr_rawgen prtac x ++ a) x (mt()))
+      hov 0 (fold_list0 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt()))
   | List1ArgType _ ->
-      hov 0 (fold_list1 (fun x a -> pr_rawgen prtac x ++ a) x (mt()))
-  | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prtac) (mt()) x)
+      hov 0 (fold_list1 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt()))
+  | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prc prtac) (mt()) x)
   | PairArgType _ ->
       hov 0
         (fold_pair
-	  (fun a b -> pr_rawgen prtac a ++ spc () ++ pr_rawgen prtac b)
+	  (fun a b -> pr_rawgen prc prtac a ++ spc () ++ pr_rawgen prc
+  prtac b)
 	  x)
   | ExtraArgType s -> 
-      try fst (Stringmap.find s !genarg_pprule) x
+      let tab = if Options.do_translate() then !genarg_pprule
+        else !genarg_pprule_v7 in
+      try fst (Stringmap.find s tab) x
       with Not_found -> str " [no printer for " ++ str s ++ str "] "
 
-let rec pr_raw_tacarg_using_rule pr_gen = function
-  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_raw_tacarg_using_rule pr_gen (l,al)
-  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_raw_tacarg_using_rule  pr_gen (l,al)
-  | [], [] -> mt ()
-  | _ -> failwith "Inconsistent arguments of extended tactic"
-
-let pr_raw_extend prt s l =
+let pr_raw_extend prc prt s l =
+  let prg = pr_rawgen prc prt in
+  let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in
   try 
-    let (s,pl) = fst (Hashtbl.find prtac_tab s) l in
-    str s ++ pr_raw_tacarg_using_rule (pr_rawgen prt) (pl,l)
+    let (s,pl) = fst (Hashtbl.find tab s) l in
+    str s ++ pr_tacarg_using_rule prg (pl,l)
   with Not_found ->
-    str "TODO(" ++ str s ++ prlist (pr_rawgen prt) l ++ str ")"
+    str "TODO(" ++ str s ++ prlist prg l ++ str ")"
 
 open Closure
 
@@ -284,23 +303,21 @@ let rec pr_generic prtac x =
 	  (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b)
 	  x)
   | ExtraArgType s -> 
-      try snd (Stringmap.find s !genarg_pprule) x
+      let tab = if Options.do_translate() then !genarg_pprule
+        else !genarg_pprule_v7 in
+      try snd (Stringmap.find s tab) x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
-let rec pr_tacarg_using_rule prt = function
-  | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule prt (l,al)
-  | Egrammar.TacNonTerm _ :: l, a :: al -> pr_generic prt a ++ pr_tacarg_using_rule prt (l,al)
-  | [], [] -> mt ()
-  | _ -> failwith "Inconsistent arguments of extended tactic"
-
 let pr_extend prt s l =
+  let prg = pr_generic prt in
+  let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in
   try 
-    let (s,pl) = snd (Hashtbl.find prtac_tab s) l in
-    str s ++ pr_tacarg_using_rule prt (pl,l)
+    let (s,pl) = snd (Hashtbl.find tab s) l in
+    str s ++ pr_tacarg_using_rule prg (pl,l)
   with Not_found ->
-    str s ++ prlist (pr_generic prt) l
+    str s ++ prlist prg l
 
-let make_pr_tac (pr_constr,pr_cst,pr_ind,pr_ident,pr_extend) =
+let make_pr_tac (pr_constr,pr_pattern,pr_cst,pr_ind,pr_ident,pr_extend) =
 
 let pr_bindings = pr_bindings pr_constr in
 let pr_with_bindings = pr_with_bindings pr_constr in
@@ -445,7 +462,7 @@ and pr_atom1 = function
   (* Constructors *)
   | TacLeft l -> hov 1 (str "Left" ++ pr_bindings l)
   | TacRight l -> hov 1 (str "Right" ++ pr_bindings l)
-  | TacSplit l -> hov 1 (str "Split" ++ pr_bindings l)
+  | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l)
   | TacAnyConstructor (Some t) ->
       hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t)
   | TacAnyConstructor None as t -> pr_atom0 t
@@ -546,13 +563,15 @@ and pr6 = function
       hov 0 (str "Match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc()
         ++ str "With"
         ++ prlist
-	  (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule true prtac r)
+	  (fun r -> fnl () ++ str "|" ++ spc () ++
+            pr_match_rule true prtac r)
 	lrul)
   | TacMatchContext (lr,lrul) ->
       hov 0 (
 	str (if lr then "Match Reverse Context With" else "Match Context With")
 	++ prlist
-	  (fun r -> fnl () ++ str "|" ++ spc () ++ pr_match_rule false prtac r)
+	  (fun r -> fnl () ++ str "|" ++ spc () ++
+            pr_match_rule false prtac r)
 	lrul)
   | TacFun (lvar,body) ->
       hov 0 (str "Fun" ++
@@ -586,10 +605,11 @@ in (prtac,pr0,pr_match_rule)
 let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) =
   make_pr_tac
     (Ppconstr.pr_constr,
+     Ppconstr.pr_constr,
      pr_metanum pr_reference,
      pr_reference,
      pr_or_meta (fun (loc,id) -> pr_id id),
-     pr_raw_extend)
+     pr_raw_extend Ppconstr.pr_constr)
 
 let _ = pr_rawtac := pr_raw_tactic
 let _ = pr_rawtac0 := pr_raw_tactic0
@@ -597,7 +617,9 @@ let _ = pr_rawtac0 := pr_raw_tactic0
 let (pr_tactic,_,_) =
   make_pr_tac
     (Printer.prterm,
+     Ppconstr.pr_constr,
      pr_evaluable_reference,
      pr_inductive,
      pr_id,
      pr_extend)
+
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index ca16c21e5..186a726f6 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -13,20 +13,24 @@ open Genarg
 open Tacexpr
 open Pretyping
 open Proof_type
+open Topconstr
 
+(* if the boolean is false then the extension applies only to old syntax *)
 val declare_extra_genarg_pprule : 
+  bool ->
   ('a raw_abstract_argument_type * ('a -> std_ppcmds)) ->
   ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit 
 
+(* idem *)
 val declare_extra_tactic_pprule : 
-  string ->
+  bool -> string ->
     (raw_generic_argument list ->
       string * Egrammar.grammar_tactic_production list)
     -> (closed_generic_argument list ->
       string * Egrammar.grammar_tactic_production list)
       -> unit 
 
-val pr_match_pattern : Tacexpr.pattern_expr match_pattern -> std_ppcmds
+val pr_match_pattern : pattern_expr match_pattern -> std_ppcmds
 
 val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) ->
   (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds
@@ -34,3 +38,18 @@ val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) ->
 val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
 
 val pr_tactic : Proof_type.tactic_expr -> std_ppcmds
+
+val pr_rawgen:
+  (constr_expr -> std_ppcmds) ->
+  (raw_tactic_expr -> std_ppcmds) ->
+    (constr_expr, raw_tactic_expr) generic_argument ->
+      std_ppcmds
+val pr_raw_extend:
+  (constr_expr -> std_ppcmds) ->
+  (raw_tactic_expr -> std_ppcmds) -> string ->
+    (constr_expr, raw_tactic_expr) generic_argument list ->
+      std_ppcmds
+val pr_extend :
+  (raw_tactic_expr -> std_ppcmds) -> string ->
+    (Term.constr, raw_tactic_expr) generic_argument list ->
+      std_ppcmds
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4404c1929..648d4690d 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -411,12 +411,6 @@ let print_local_context () =
   in 
   (print_var_rec env ++  print_last_const env)
 
-let fprint_var name typ =
-  (str ("*** [" ^ name ^ " :") ++ fprtype typ ++ str "]" ++ fnl ())
-
-let fprint_judge {uj_val=trm;uj_type=typ} = 
-  (fprterm trm ++ str" : " ++ fprterm typ)
-
 let unfold_head_fconst = 
   let rec unfrec k = match kind_of_term k with
     | Const cst -> constant_value (Global.env ()) cst 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 72fe499e6..df2aabdf8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -28,15 +28,91 @@ open Ppconstr
 
 let emacs_str s = if !Options.print_emacs then s else "" 
 
-(* These are the names of the universes where the pp rules for constr and
-   tactic are put (must be consistent with files PPConstr.v and PPTactic.v *)
-
-let tactic_syntax_universe = "tactic"
+(**********************************************************************)
+(* Old Ast printing *)
 
+let constr_syntax_universe = "constr"
 (* This is starting precedence for printing constructions or tactics *)
 (* Level 9 means no parentheses except for applicative terms (at level 10) *)
-let tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Ppextend.L)
-
+let constr_initial_prec_v7 = Some (9,Ppextend.L)
+let constr_initial_prec = Some (200,Ppextend.E)
+
+let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
+
+let global_const_name kn =
+  try pr_global Idset.empty (ConstRef kn)
+  with Not_found -> (* May happen in debug *)
+    (str ("CONST("^(string_of_kn kn)^")"))
+
+let global_var_name id =
+  try pr_global Idset.empty (VarRef id)
+  with Not_found -> (* May happen in debug *)
+    (str ("SECVAR("^(string_of_id id)^")"))
+
+let global_ind_name (kn,tyi) =
+  try pr_global Idset.empty (IndRef (kn,tyi))
+  with Not_found -> (* May happen in debug *)
+    (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
+
+let global_constr_name ((kn,tyi),i) =
+  try pr_global Idset.empty (ConstructRef ((kn,tyi),i))
+  with Not_found -> (* May happen in debug *)
+    (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
+		  ^","^(string_of_int i)^")"))
+
+let globpr gt = match gt with
+  | Nvar(_,s) -> (pr_id s)
+  | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
+  | Node(_,"CONST",[Path(_,sl)]) ->
+      global_const_name (section_path sl)
+  | Node(_,"SECVAR",[Nvar(_,s)]) ->
+      global_var_name s
+  | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
+      global_ind_name (section_path sl, tyi)
+  | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
+      global_constr_name ((section_path sl, tyi), i)
+  | Dynamic(_,d) ->
+    if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
+    else dfltpr gt
+  | gt -> dfltpr gt
+
+
+let wrap_exception = function
+    Anomaly (s1,s2) ->
+      warning ("Anomaly ("^s1^")"); pp s2;
+      str"<PP error: non-printable term>"
+  | Failure _ | UserError _ | Not_found ->
+      str"<PP error: non-printable term>"
+  | s -> raise s
+
+let gentermpr_fail gt =
+  let prec =
+    if !Options.v7 then constr_initial_prec_v7 else constr_initial_prec in
+  Esyntax.genprint globpr constr_syntax_universe prec gt
+
+let gentermpr gt =
+  try gentermpr_fail gt
+  with s -> wrap_exception s
+
+(**********************************************************************)
+(* Generic printing: choose old or new printers *)
+
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+  if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
+  else Ppconstrnew.pr_constr (Constrextern.extern_constr at_top env t)
+let pr_cases_pattern t =
+  if !Options.v7 then gentermpr (Termast.ast_of_cases_pattern t)
+  else Ppconstrnew.pr_cases_pattern
+    (Constrextern.extern_cases_pattern Idset.empty t)
+let pr_pattern_env tenv env t =
+  if !Options.v7 then gentermpr (Termast.ast_of_pattern tenv env t)
+  else Ppconstrnew.pr_constr
+    (Constrextern.extern_pattern tenv env t)
+
+(**********************************************************************)
+(* Derived printers *)
+  
 let prterm_env_at_top env = gentermpr_core true env
 let prterm_env env = gentermpr_core false env
 let prtype_env env typ = prterm_env env typ
@@ -48,25 +124,14 @@ let prterm t = prterm_env (Global.env()) t
 let prtype t = prtype_env (Global.env()) t
 let prjudge j = prjudge_env (Global.env()) j
 
-let fprterm_env a =
-  warning "Fw printing not implemented, use CCI printing 1"; prterm_env a
-let fprterm a =
-  warning "Fw printing not implemented, use CCI printing 2"; prterm a
-
-let fprtype_env env typ =
-  warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ
-let fprtype a =
-  warning "Fw printing not implemented, use CCI printing 4"; prtype a
+let pr_constant env cst = prterm_env env (mkConst cst)
+let pr_existential env ev = prterm_env env (mkEvar ev)
+let pr_inductive env ind = prterm_env env (mkInd ind)
+let pr_constructor env cstr = prterm_env env (mkConstruct cstr)
+let pr_global = pr_global Idset.empty
 
-(* For compatibility *)
-let fterm0 = fprterm_env
-
-let pr_constant env cst = gentermpr (ast_of_constant env cst)
-let pr_existential env ev = gentermpr (ast_of_existential env ev)
-let pr_inductive env ind = gentermpr (ast_of_inductive env ind)
-let pr_constructor env cstr = gentermpr (ast_of_constructor env cstr)
-
-let pr_global = pr_global
+let pr_rawterm t =
+  pr_constr (Constrextern.extern_rawconstr Idset.empty t)
 
 open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
@@ -75,49 +140,8 @@ let pr_ref_label = function (* On triche sur le contexte *)
   | CstrNode sp -> pr_constructor (Global.env()) sp
   | VarNode id -> pr_id id
 
-let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
-(*
-let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
-*)
-let pr_rawterm t = pr_constr (Constrextern.extern_rawconstr t)
-let pr_pattern_env tenv env t = gentermpr (Termast.ast_of_pattern tenv env t)
 let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
 
-(*
-let gentacpr x = Pptactic.prtac x
-*)
-
-(*
-and default_tacpr = function
-    | Nvar(_,s) -> (pr_id s)
-
-    (* constr's may occur inside tac expressions ! *)
-    | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
-    | Node(_,"CONST",[Path(_,sl)]) ->
-	let sp = section_path sl in
-	pr_global (ConstRef sp)
-    | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
-	let sp = section_path sl in
-	pr_global (IndRef (sp,tyi))
-    | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
-	let sp = section_path sl in
-	pr_global (ConstructRef ((sp,tyi),i))
-
-    (* This should be tactics *)
-    | Node(_,s,[]) -> (str s)
-(* TODO
-    | Node(_,s,ta) ->
-	(str s ++ brk(1,2) ++ hov 0 (prlist_with_sep pr_spc gentacpr ta))
-*)
-    | Dynamic(_,d) as gt ->
-      let tg = Dyn.tag d in
-      if tg = "tactic" then (str"<dynamic [tactic]>")
-      else if tg = "value" then (str"<dynamic [value]>")
-      else if tg = "constr" then (str"<dynamic [constr]>")
-      else dfltpr gt
-    | gt -> dfltpr gt 
-*)
-
 let pr_var_decl env (id,c,typ) =
   let pbody = match c with
     | None ->  (mt ())
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 48ee955cc..b69a9955b 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -58,13 +58,3 @@ val pr_context_of   : env -> std_ppcmds
 
 val emacs_str       : string -> string
 
-(*i*) 
-val fprterm_env     : env -> constr -> std_ppcmds
-val fprterm         : constr -> std_ppcmds
-val fprtype_env     : env -> types -> std_ppcmds
-val fprtype         : types -> std_ppcmds
-
-(* For compatibility *)
-val fterm0          : env -> constr -> std_ppcmds
-(*i*)
-
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 1f352f6af..2b3967707 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -407,8 +407,9 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacLeft $mlexpr_of_binding_kind l$>>
   | Tacexpr.TacRight l ->
       <:expr< Tacexpr.TacRight $mlexpr_of_binding_kind l$>>
-  | Tacexpr.TacSplit l ->
-      <:expr< Tacexpr.TacSplit $mlexpr_of_binding_kind l$>>
+  | Tacexpr.TacSplit (b,l) ->
+      <:expr< Tacexpr.TacSplit
+        ($mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>>
   | Tacexpr.TacAnyConstructor t ->
       <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_option mlexpr_of_tactic t$>>
   | Tacexpr.TacConstructor (n,l) ->
diff --git a/parsing/search.ml b/parsing/search.ml
index 74cdd77dd..fc5792fa0 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -107,7 +107,7 @@ let plain_display ref a c =
 let filter_by_module (module_list:dir_path list) (accept:bool) 
   (ref:global_reference) _ _ =
   try
-    let sp = sp_of_global None ref in
+    let sp = sp_of_global ref in
     let sl = dirpath sp in
     let rec filter_aux = function
       | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 593fb0169..a3d5f496e 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -124,7 +124,16 @@ let make_printing_rule l =
     (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
   List.fold_right add_printing_clause l [default]
 
-let declare_tactic loc s cl =
+let new_tac_ext (s,cl) =
+  (String.lowercase s, List.map 
+    (fun (s,l,e) ->
+      (String.lowercase s, List.map
+        (function TacTerm s -> TacTerm (String.lowercase s)
+          | t -> t) l,
+        e))
+    cl)
+
+let declare_tactic_v7 loc s cl =
   let pl = make_printing_rule cl in
   let gl = mlexpr_of_clause cl in
   let hide_tac (_,p,e) =
@@ -142,13 +151,44 @@ let declare_tactic loc s cl =
   <:str_item<
     declare
       open Pcoq;
-      declare $list:List.map hide_tac cl$ end;
+      Egrammar.extend_tactic_grammar $se$ $gl$;
+      let pp = fun [ $list:pl$ ] in
+      Pptactic.declare_extra_tactic_pprule False $se$ pp pp;
+    end
+  >>
+
+let declare_tactic loc s cl =
+  let (s',cl') = new_tac_ext (s,cl) in
+  let pl' = make_printing_rule cl' in
+  let gl' = mlexpr_of_clause cl' in
+  let se' = mlexpr_of_string s' in
+  let pl = make_printing_rule cl in
+  let gl = mlexpr_of_clause cl in
+  let hide_tac (_,p,e) =
+    (* reste a definir les fonctions cachees avec des noms frais *)
+    let stac = "h_"^s' in
+    let e = 
+      make_fun
+        <:expr<
+          Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $e$
+        >>
+      p in
+    <:str_item< value $lid:stac$ = $e$ >>
+  in
+  let se = mlexpr_of_string s in
+  <:str_item<
+    declare
+      open Pcoq;
+      declare $list:List.map hide_tac cl'$ end;
       try
-       Refiner.add_tactic $se$ (fun [ $list:make_clauses s cl$ ])
+       Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ])
       with e -> Pp.pp (Cerrors.explain_exn e);
-      Egrammar.extend_tactic_grammar $se$ $gl$;
+      Egrammar.extend_tactic_grammar $se'$ $gl'$;
+      let pp' = fun [ $list:pl'$ ] in
+      Pptactic.declare_extra_tactic_pprule True $se'$ pp' pp';
+      Egrammar.extend_tactic_grammar $se'$ $gl$;
       let pp = fun [ $list:pl$ ] in
-      Pptactic.declare_extra_tactic_pprule $se$ pp pp;
+      Pptactic.declare_extra_tactic_pprule False $se'$ pp pp;
     end
   >>
 
@@ -194,7 +234,11 @@ EXTEND
     [ [ "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
-         declare_tactic loc s l ] ]
+         declare_tactic loc s l
+      | "V7"; "TACTIC"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        OPT "|"; l = LIST1 tacrule SEP "|";
+        "END" ->
+         declare_tactic_v7 loc s l ] ]
   ;
   tacrule:
     [ [ "["; s = STRING; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"