Nettoyage des fichiers de parsing

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

13 files changed, 561 insertions, 678 deletions

diff --git a/.depend b/.depend
index 6dfd64e554..c086caa0ca 100644
--- a/.depend
+++ b/.depend
@@ -71,10 +71,6 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
-pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \
@@ -605,12 +601,14 @@ pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \
     library/summary.cmx pretyping/syntax_def.cmi 
 pretyping/tacred.cmo: kernel/closure.cmi library/declare.cmi \
     kernel/environ.cmi kernel/generic.cmi kernel/inductive.cmi \
-    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi library/redinfo.cmi \
-    kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi 
+    kernel/instantiate.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
+    library/redinfo.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+    lib/util.cmi pretyping/tacred.cmi 
 pretyping/tacred.cmx: kernel/closure.cmx library/declare.cmx \
     kernel/environ.cmx kernel/generic.cmx kernel/inductive.cmx \
-    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx library/redinfo.cmx \
-    kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi 
+    kernel/instantiate.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
+    library/redinfo.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+    lib/util.cmx pretyping/tacred.cmi 
 pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
     kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi 
@@ -833,8 +831,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/generic.cmx library/global.cmx proofs/logic.cmx kernel/names.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi 
-tools/coqdep.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \
     parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi library/indrec.cmi \
diff --git a/Makefile b/Makefile
index af53a8121d..76dba4437e 100644
--- a/Makefile
+++ b/Makefile
@@ -82,7 +82,7 @@ PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \
 	  pretyping/syntax_def.cmo
 
 PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
-	parsing/g_prim.cmo parsing/g_corevernac.cmo parsing/g_basevernac.cmo \
+	parsing/g_prim.cmo parsing/g_basevernac.cmo \
 	parsing/g_vernac.cmo parsing/g_tactic.cmo \
 	parsing/g_constr.cmo parsing/g_cases.cmo \
         parsing/extend.cmo parsing/termast.cmo \
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 3064492d33..2068bd9dcd 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -7,17 +7,15 @@ open Pcoq
 open Vernac
 
 GEXTEND Gram
+  GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list
+          stringarg ne_stringarg_list constrarg sortarg tacarg;
+
   identarg:
     [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
   ;
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
-
-  ne_identarg_comma_list:
-    [ [ id = identarg; ","; idl = ne_identarg_comma_list -> id::idl
-      | id = identarg -> [id] ] ]
-  ;
   numarg:
     [ [ n = Prim.number -> n 
        |  "-"; n = Prim.number -> Num (loc, ( - Ast.num_of_ast n)) ] ]
@@ -33,24 +31,25 @@ GEXTEND Gram
   stringarg:
     [ [ s = Prim.string -> s ] ]
   ;
-  comarg:
-    [ [ c = Constr.constr -> <:ast< (CONSTR $c) >> ] ]
-  ;
-  lcomarg:
-    [ [ c = Constr.lconstr -> <:ast< (CONSTR $c) >> ] ]
-  ;
-  lvernac:
-    [ [ v = vernac; l = lvernac -> v::l
-      |  -> [] ] ]
-  ;
   ne_stringarg_list:
     [ [ n = stringarg; l = ne_stringarg_list -> n::l
       | n = stringarg -> [n] ] ]
   ;
-  varg_ne_stringarg_list:
-    [ [ l = ne_stringarg_list -> <:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
+  constrarg:
+    [ [ c = Constr.constr -> <:ast< (CONSTR $c) >> ] ]
+  ;
+  sortarg:
+    [ [ c = Constr.sort -> <:ast< (CONSTR $c) >> ] ]
   ;
-  vernac:
+  tacarg:
+    [ [ tcl = Tactic.tactic_com_list -> tcl ] ]
+  ;
+END;
+
+GEXTEND Gram
+  GLOBAL: command;
+
+  command:
     [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
       | IDENT "Cd"; "." -> <:ast< (CD) >>
       | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
@@ -91,13 +90,13 @@ GEXTEND Gram
       | IDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
       | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
       (* TODO: rapprocher Eval et Check *)
-      | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = comarg; "." ->
+      | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg; "." ->
           <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
       | IDENT "Eval"; g = numarg; r = Tactic.red_tactic;
-        "in"; c = comarg; "." ->
+        "in"; c = constrarg; "." ->
           <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
-      | check = check_tok; c = comarg; "." -> <:ast< (Check $check $c) >>
-      | check = check_tok; g = numarg; c = comarg; "." ->
+      | check = check_tok; c = constrarg; "." -> <:ast< (Check $check $c) >>
+      | check = check_tok; g = numarg; c = constrarg; "." ->
           <:ast< (Check $check $c $g) >>
       | IDENT "Print"; IDENT "ML"; IDENT "Path"; "." ->
           <:ast< (PrintMLPath) >>
@@ -118,7 +117,7 @@ GEXTEND Gram
       | IDENT "Untime"; "." -> <:ast< (Untime) >> *)
 
       | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
-      | IDENT "SearchIsos"; com = comarg; "." ->
+      | IDENT "SearchIsos"; com = constrarg; "." ->
           <:ast< (Searchisos $com) >>
       | "Set"; IDENT "Undo"; n = numarg; "." ->
           <:ast< (SETUNDO $n) >>
@@ -170,3 +169,112 @@ GEXTEND Gram
       | "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
   ;
 END;
+
+(* Grammar extensions *)
+	  
+GEXTEND Gram
+  GLOBAL: syntax_command Prim.syntax_entry Prim.grammar_entry;
+
+  syntax_command:
+   [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
+
+     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
+         <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
+
+     | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
+         <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >>
+     | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
+       p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
+     | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
+       p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
+     | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
+         <:ast< (PrintGrammar $uni $ent) >>
+  ] ]
+  ;
+
+  (* Syntax entries for Grammar. Only grammar_entry is exported *)
+  Prim.grammar_entry:
+    [[ nont = Prim.ident; etyp = Prim.entry_type; ":=";
+       ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
+         <:ast< (GRAMMARENTRY $nont $etyp $ep ($LIST rl)) >> ]]
+  ;
+  entry_prec:
+    [[ IDENT "LEFTA" -> <:ast< {LEFTA} >>
+     | IDENT "RIGHTA" -> <:ast< {RIGHTA} >>
+     | IDENT "NONA" -> <:ast< {NONA} >>
+     | ->  <:ast< {NONE} >> ] ]
+  ;
+  grammar_rule:
+    [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
+       a = Prim.astact ->
+        <:ast< (GRAMMARRULE ($ID name) $a ($LIST pil)) >> ]]
+  ;
+  rule_name:
+    [[ name = IDENT -> name ]]
+  ;
+  production_item:
+    [[ s = STRING -> <:ast< ($STR $s) >>
+     | nt = non_terminal; po = OPT [ "("; p = Prim.ident; ")" -> p ] ->
+         match po with
+           | Some p -> <:ast< (NT $nt $p) >>
+           | _ -> <:ast< (NT $nt) >> ]]
+  ;
+  non_terminal:
+    [[ u = Prim.ident; ":"; nt = Prim.ident -> <:ast< (QUAL $u $nt) >>
+     | nt = Prim.ident -> <:ast< $nt >> ]]
+  ;
+
+
+  (* Syntax entries for Syntax. Only syntax_entry is exported *)
+  Prim.syntax_entry:
+    [ [ IDENT "level"; p = precedence; ":";
+	OPT "|"; rl = LIST1 syntax_rule SEP "|" ->
+          <:ast< (SYNTAXENTRY $p ($LIST $rl)) >> ] ]
+  ;
+  syntax_rule:
+    [ [ nm = IDENT; "["; s = Prim.astpat; "]"; "->"; u = unparsing ->
+          <:ast< (SYNTAXRULE ($ID $nm) $s $u) >> ] ]
+  ;
+  precedence:
+    [ [ a = Prim.number ->  <:ast< (PREC $a 0 0) >>
+      | "["; a1 = Prim.number; a2 = Prim.number; a3 = Prim.number; "]" ->
+          <:ast< (PREC $a1 $a2 $a3) >> ] ]
+  ;
+  unparsing:
+    [ [ "["; ll = LIST0 next_hunks; "]" -> <:ast< (UNPARSING ($LIST $ll))>> ] ]
+  ;
+  next_hunks:
+    [ [ IDENT "FNL" -> <:ast< (UNP_FNL) >>
+      | IDENT "TAB" -> <:ast< (UNP_TAB) >>
+      | c = STRING -> <:ast< (RO ($STR $c)) >>
+      | "[";
+        x =
+          [ b = box; ll = LIST0 next_hunks -> <:ast<(UNP_BOX $b ($LIST $ll))>>
+          | n = Prim.number; m = Prim.number -> <:ast< (UNP_BRK $n $m) >>
+          | IDENT "TBRK";
+            n = Prim.number; m = Prim.number -> <:ast< (UNP_TBRK $n $m) >> ];
+        "]" -> x
+      | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] ->
+          match oprec with
+	    | Some pr -> <:ast< (PH $e $pr) >>
+            | None -> <:ast< (PH $e {Any}) >> ]]
+  ;
+  box:
+    [ [ "<"; bk = box_kind; ">" -> bk ] ]
+  ;
+  box_kind:
+    [ [ IDENT "h"; n = Prim.number -> <:ast< (PpHB $n) >>
+      | IDENT "v"; n = Prim.number -> <:ast< (PpVB $n) >>
+      | IDENT "hv"; n = Prim.number -> <:ast< (PpHVB $n) >>
+      | IDENT "hov"; n = Prim.number -> <:ast< (PpHOVB $n) >>
+      | IDENT "t" -> <:ast< (PpTB) >> ] ]
+  ;
+  paren_reln_or_extern:
+    [ [ IDENT "L" -> <:ast< {L} >>
+      | IDENT "E" -> <:ast< {E} >>
+      | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
+	  match precrec with
+	    | Some p -> <:ast< (EXTERN ($STR $pprim) $p) >>
+            | None -> <:ast< (EXTERN ($STR $pprim)) >> ] ]
+  ;
+END
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3640db1bc7..dd328059f7 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -7,7 +7,7 @@ open Constr
 GEXTEND Gram
   GLOBAL: ident constr0 constr1 constr2 constr3 lassoc_constr4 constr5
           constr6 constr7 constr8 constr9 constr10 lconstr constr
-          ne_ident_comma_list ne_constr_list;
+          ne_ident_comma_list ne_constr_list sort ne_binders_list;
 
   ident:
     [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
@@ -25,22 +25,15 @@ GEXTEND Gram
     [ [ c1 = constr; cl = ne_constr_list -> c1::cl
       | c1 = constr -> [c1] ] ]
   ;
+  sort:
+    [ [ "Set"  -> <:ast< (SET) >>
+      | "Prop" -> <:ast< (PROP) >>
+      | "Type" -> <:ast< (TYPE) >> ] ]
+  ;
   constr0:
     [ [ "?" -> <:ast< (ISEVAR) >>
       | "?"; n = Prim.number -> <:ast< (META $n) >>
-      | "["; id1 = IDENT; ":"; c = constr; c2 = abstraction_tail ->
-          <:ast< (LAMBDALIST $c [$id1]$c2) >>
-      | "["; id1 = IDENT; ","; idl = ne_ident_comma_list;
-        ":"; c = constr; c2 = abstraction_tail ->
-          <:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >>
-      | "["; id1 = IDENT; ","; idl = ne_ident_comma_list;
-             c = abstraction_tail ->
-          <:ast< (LAMBDALIST (ISEVAR) [$id1]($SLAM $idl $c)) >>
-      | "["; id1 = IDENT; c = abstraction_tail ->
-          <:ast< (LAMBDALIST (ISEVAR) [$id1]$c) >>
-      | "["; id1 = IDENT; "="; c = constr; "]"; c2 = constr ->
-          <:ast< (ABST #Core#let.cci $c [$id1]$c2) >> 
-      | "<<"; id1 = IDENT; ">>"; c = constr -> <:ast< [$id1]$c >>
+      | bl = binders; c = constr -> <:ast< ($ABSTRACT "LAMBDALIST" $bl $c) >>
       | "("; lc1 = lconstr; ":"; c = constr; body = product_tail ->
           let id = Ast.coerce_to_var "lc1" lc1 in
             <:ast< (PROD $c [$id]$body) >>
@@ -59,13 +52,11 @@ GEXTEND Gram
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
           <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
 *)
-      | "Prop" -> <:ast< (PROP) >>
-      | "Set"  -> <:ast< (SET) >>
-      | "Type" -> <:ast< (TYPE) >>
       | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
           <:ast< (FIX $id ($LIST $fbinders)) >>
       | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
           <:ast< (COFIX $id ($LIST $fbinders)) >>
+      | s = sort -> s
       | v = ident -> v ] ]
   ;
   constr1:
@@ -107,7 +98,7 @@ GEXTEND Gram
           <:ast< (CASE "NOREC" $l1 $c1 $c2 $c3) >>
       | c = constr0 -> c ] ]
   ;
-  constr2:
+  constr2: (* ~ will be here *)
     [ [ c = constr1 -> c ] ]
   ;
   constr3:
@@ -117,23 +108,21 @@ GEXTEND Gram
     [ [ c1 = constr3 -> c1 ] ]
   ;
   constr5:
-    [ [ c1 = lassoc_constr4 -> c1
-      | c1 = lassoc_constr4; "::"; c2 = constr5 ->
-          <:ast< (CAST $c1 $c2) >> ] ]
+    [ [ c1 = lassoc_constr4 -> c1 ] ]
   ;
-  constr6:
+  constr6:  (* /\ will be here *)
     [ [ c1 = constr5 -> c1 ] ]
   ;
-  constr7:
+  constr7:  (* \/ will be here *)
     [ RIGHTA [ c1 = constr6 -> c1 ] ]
   ;
-  constr8:
+  constr8:  (* <-> will be here *)
     [ [ c1 = constr7 -> c1
-      | c1 = constr7; "->"; c2 = constr8 ->
-          <:ast< (PROD $c1 [<>]$c2) >> ] ]
+      | c1 = constr7; "->"; c2 = constr8 -> <:ast< (PROD $c1 [<>]$c2) >> ] ]
   ;
   constr9:
-    [ [ c1 = constr8 -> c1 ] ]
+    [ [ c1 = constr8 -> c1
+      | c1 = constr8; "::"; c2 = constr8 -> <:ast< (CAST $c1 $c2) >> ] ]
   ;
   constr10:
     [ [ "!"; f = IDENT; args = ne_constr9_list ->
@@ -143,30 +132,35 @@ GEXTEND Gram
       | f = constr9 -> f ] ]
   ;
   ne_ident_comma_list:
-    [ [ id = ident; ","; idl = ne_ident_comma_list -> id::idl
+    [ [ id = ident; ","; idl = ne_ident_comma_list -> id :: idl
       | id = ident -> [id] ] ]
   ;
-  binder:
-    [ [ idl = ne_ident_comma_list; c = type_option ->
-          <:ast< (BINDER $c ($LIST $idl)) >> ] ]
+  ident_comma_list_tail:
+    [ [ ","; idl = ne_ident_comma_list -> idl
+      | -> [] ] ]
+  ;
+  vardecls:
+    [ [ id = ident; idl = ident_comma_list_tail; c = type_option ->
+          <:ast< ($BINDER $c $id ($LIST $idl)) >>
+      | id = ident; "="; c = constr ->
+	  <:ast< (ABST #Core#let.cci $c $id) >> ] ]
+  ;
+  ne_vardecls_list:
+    [ [ id = vardecls; ";"; idl = ne_vardecls_list -> id :: idl
+      | id = vardecls -> [id] ] ]
   ;
-  ne_binder_list:
-    [ [ id = binder; ";"; idl = ne_binder_list -> id::idl
-      | id = binder -> [id] ] ]
+  binders:
+    [ [ "["; bl = ne_vardecls_list; "]" -> bl ] ]
+  ;
+  ne_binders_list:
+    [ [ bl = binders; bll = ne_binders_list -> bl @ bll
+      | bl = binders -> bl ] ]
   ;
   type_option:
     [ [ ":"; c = constr -> c 
       | -> <:ast< (ISEVAR) >> ] ]
   ;
-(*  parameters:
-    [ [ "["; bl = ne_binder_semi_list; "]" -> $bl ] ]
-  ;
-  parameters_list:
-    [ [ 
-          <:ast< (BINDERLIST ($LIST $bl)) >>
-      |  -> <:ast< (BINDERLIST) >> ] ]
-  ;
-*)  constr91:
+  constr91:
     [ [ n = Prim.number; "!"; c1 = constr9 ->
           <:ast< (EXPL $n $c1) >>
       | c1 = constr9 -> c1 ] ]
@@ -182,7 +176,7 @@ GEXTEND Gram
   fixbinder:
     [ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = constr;
         ":="; def = constr -> <:ast< (NUMFDECL $id $recarg $type_ $def) >>
-      | id = ident; "["; idl = ne_binder_list; "]"; ":"; type_ = constr;
+      | id = ident; idl = ne_binders_list; ":"; type_ = constr;
         ":="; def = constr ->
           <:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ]
   ;
@@ -198,14 +192,6 @@ GEXTEND Gram
     [ [ fb = cofixbinder; "with"; fbs = cofixbinders -> fb::fbs
       | fb = cofixbinder -> [fb] ] ]
   ;
-  abstraction_tail:
-    [ [ ";"; idl = ne_ident_comma_list;
-        ":"; c = constr; c2 = abstraction_tail ->
-          <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >>
-      | ";"; idl = ne_ident_comma_list; c2 = abstraction_tail ->
-          <:ast< (LAMBDALIST (ISEVAR) ($SLAM $idl $c2)) >>
-      | "]"; c = constr -> c ] ]
-  ;
   product_tail:
     [ [ ";"; idl = ne_ident_comma_list;
         ":"; c = constr; c2 = product_tail ->
diff --git a/parsing/g_corevernac.ml4 b/parsing/g_corevernac.ml4
deleted file mode 100644
index b8f5b30394..0000000000
--- a/parsing/g_corevernac.ml4
+++ /dev/null
@@ -1,137 +0,0 @@
-
-(* $Id$ *)
-
-(* These are the entries without which MakeBare cannot be compiled *)
-
-open Pcoq
-
-open Vernac
-
-GEXTEND Gram
-  vernac:
-    [ RIGHTA
-
-     [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
-       s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
-         <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
-
-     | "Compile";
-       verbosely =
-         [ IDENT "Verbose" -> "Verbose"
-         | -> "" ];
-       IDENT "Module";
-       only_spec =
-         [ IDENT "Specification" -> "Specification"
-         | -> "" ];
-       mname = [ s = STRING -> s | s = IDENT -> s ];
-       fname = OPT [ s = STRING -> s | s = IDENT -> s ]; "." ->
-         let fname = match fname with Some s -> s | None -> mname in
-         <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
-                   ($STR $mname) ($STR $fname))>> ]]
-  ;
-END
-
-GEXTEND Gram
-  GLOBAL: vernac Prim.syntax_entry Prim.grammar_entry;
-
-  vernac:
-    [[ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
-
-     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
-         <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
-
-     | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
-         <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >>
-     | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
-       p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
-     | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
-       p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> ]]
-  ;
-
-  (* Syntax entries for Grammar. Only grammar_entry is exported *)
-  Prim.grammar_entry:
-    [[ nont = Prim.ident; etyp = Prim.entry_type; ":=";
-       ep = entry_prec; OPT "|"; rl = LIST0 grammar_rule SEP "|" ->
-         <:ast< (GRAMMARENTRY $nont $etyp $ep ($LIST rl)) >> ]]
-  ;
-  entry_prec:
-    [[ IDENT "LEFTA" -> <:ast< {LEFTA} >>
-     | IDENT "RIGHTA" -> <:ast< {RIGHTA} >>
-     | IDENT "NONA" -> <:ast< {NONA} >>
-     | ->  <:ast< {NONE} >> ] ]
-  ;
-  grammar_rule:
-    [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
-       a = Prim.astact ->
-        <:ast< (GRAMMARRULE ($ID name) $a ($LIST pil)) >> ]]
-  ;
-  rule_name:
-    [[ name = IDENT -> name ]]
-  ;
-  production_item:
-    [[ s = STRING -> <:ast< ($STR $s) >>
-     | nt = non_terminal; po = OPT [ "("; p = Prim.ident; ")" -> p ] ->
-         match po with
-           | Some p -> <:ast< (NT $nt $p) >>
-           | _ -> <:ast< (NT $nt) >> ]]
-  ;
-  non_terminal:
-    [[ u = Prim.ident; ":"; nt = Prim.ident -> <:ast< (QUAL $u $nt) >>
-     | nt = Prim.ident -> <:ast< $nt >> ]]
-  ;
-
-
-  (* Syntax entries for Syntax. Only syntax_entry is exported *)
-  Prim.syntax_entry:
-    [ [ IDENT "level"; p = precedence; ":";
-	OPT "|"; rl = LIST1 syntax_rule SEP "|" ->
-          <:ast< (SYNTAXENTRY $p ($LIST $rl)) >> ] ]
-  ;
-  syntax_rule:
-    [ [ nm = IDENT; "["; s = Prim.astpat; "]"; "->"; u = unparsing ->
-          <:ast< (SYNTAXRULE ($ID $nm) $s $u) >> ] ]
-  ;
-  precedence:
-    [ [ a = Prim.number ->  <:ast< (PREC $a 0 0) >>
-      | "["; a1 = Prim.number; a2 = Prim.number; a3 = Prim.number; "]" ->
-          <:ast< (PREC $a1 $a2 $a3) >> ] ]
-  ;
-  unparsing:
-    [ [ "["; ll = LIST0 next_hunks; "]" -> <:ast< (UNPARSING ($LIST $ll))>> ] ]
-  ;
-  next_hunks:
-    [ [ IDENT "FNL" -> <:ast< (UNP_FNL) >>
-      | IDENT "TAB" -> <:ast< (UNP_TAB) >>
-      | c = STRING -> <:ast< (RO ($STR $c)) >>
-      | "[";
-        x =
-          [ b = box; ll = LIST0 next_hunks -> <:ast<(UNP_BOX $b ($LIST $ll))>>
-          | n = Prim.number; m = Prim.number -> <:ast< (UNP_BRK $n $m) >>
-          | IDENT "TBRK";
-            n = Prim.number; m = Prim.number -> <:ast< (UNP_TBRK $n $m) >> ];
-        "]" -> x
-      | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln_or_extern -> pr ] ->
-          match oprec with
-	    | Some pr -> <:ast< (PH $e $pr) >>
-            | None -> <:ast< (PH $e {Any}) >> ]]
-  ;
-  box:
-    [ [ "<"; bk = box_kind; ">" -> bk ] ]
-  ;
-  box_kind:
-    [ [ IDENT "h"; n = Prim.number -> <:ast< (PpHB $n) >>
-      | IDENT "v"; n = Prim.number -> <:ast< (PpVB $n) >>
-      | IDENT "hv"; n = Prim.number -> <:ast< (PpHVB $n) >>
-      | IDENT "hov"; n = Prim.number -> <:ast< (PpHOVB $n) >>
-      | IDENT "t" -> <:ast< (PpTB) >> ] ]
-  ;
-  paren_reln_or_extern:
-    [ [ IDENT "L" -> <:ast< {L} >>
-      | IDENT "E" -> <:ast< {E} >>
-      | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
-	  match precrec with
-	    | Some p -> <:ast< (EXTERN ($STR $pprim) $p) >>
-            | None -> <:ast< (EXTERN ($STR $pprim)) >> ] ]
-  ;
-END
-
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 424591efb7..3814af4f26 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -309,7 +309,8 @@ GEXTEND Gram
       | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >>
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "Change"; c = comarg; cl = clausearg ->
-	  <:ast< (Change $c $cl) >> ]
+	  <:ast< (Change $c $cl) >> 
+      | IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ]
 
     | [ id = identarg; l = comarg_list ->
           match (isMeta (nvar_of_ast id), l) with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 81f9630832..f3deaa20ec 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -3,26 +3,24 @@
 
 open Pcoq
 
-open Tactic
-
-GEXTEND Gram
-  simple_tactic:
-    [ [ IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] ]
-  ;
-END
-
 open Vernac
 
 GEXTEND Gram
+  vernac:
+    [ [ g = gallina -> g 
+      | g = gallina_ext -> g
+      | c = command -> c 
+      | c = syntax_command -> c ] ]
+  ;
   vernac: LAST
     [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ]
   ;
 END
 
+(* Gallina declarations *)
 GEXTEND Gram
-  tacarg:
-    [ [ tcl = Tactic.tactic_com_list -> tcl ] ]
-  ;
+  GLOBAL: gallina gallina_ext;
+
   theorem_body_line:
     [ [ n = numarg; ":"; tac = tacarg; "." ->
           <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >>
@@ -37,43 +35,162 @@ GEXTEND Gram
     [ [ l = theorem_body_line_list ->
           <:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
   ;
-  destruct_location :
-  [ [ IDENT "Conclusion"  -> <:ast< (CONCL)>>
-    | IDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
-    | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
+  thm_tok:
+    [ [ "Theorem" -> <:ast< "THEOREM" >>
+      | IDENT "Lemma" -> <:ast< "LEMMA" >>
+      | IDENT "Fact" -> <:ast< "FACT" >>
+      | IDENT "Remark" -> <:ast< "REMARK" >> ] ]
+  ;
+  def_tok:
+    [ [ "Definition" -> <:ast< "DEFINITION" >>
+      | IDENT "Local" -> <:ast< "LOCAL" >> 
+      | "@"; "Definition"  -> <:ast< "OBJECT" >>
+      | "@"; IDENT "Local"  -> <:ast< "LOBJECT" >>
+      | "@"; IDENT "Coercion"  -> <:ast< "OBJCOERCION" >>
+      | "@"; IDENT "Local"; IDENT "Coercion"  -> <:ast< "LOBJCOERCION" >>
+      | IDENT "SubClass"  -> <:ast< "SUBCLASS" >>
+      | IDENT "Local"; IDENT "SubClass"  -> <:ast< "LSUBCLASS" >> ] ]  
+  ;
+  hyp_tok:
+    [ [ "Hypothesis" -> <:ast< "HYPOTHESIS" >>
+      | "Variable" -> <:ast< "VARIABLE" >> ] ]
   ;
-  ne_comarg_list:
-  [ [ l = LIST1 comarg -> l ] ]
+  hyps_tok:
+    [ [ IDENT "Hypotheses" -> <:ast< "HYPOTHESES" >>
+      | IDENT "Variables" -> <:ast< "VARIABLES" >> ] ]
+  ;
+  param_tok:
+    [ [ "Axiom" -> <:ast< "AXIOM" >>
+      | "Parameter" -> <:ast< "PARAMETER" >> ] ]
+  ;
+  params_tok:
+    [ [ IDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ]
+  ;
+  params:
+    [ [ idl = Constr.ne_ident_comma_list; ":"; c = Constr.constr ->
+          <:ast< (BINDER $c ($LIST $idl)) >> ] ]
   ;
+  ne_params_list:
+    [ [ id = params; ";"; idl = ne_params_list -> id :: idl
+      | id = params -> [id] ] ]
+  ;
+  reduce:
+    [ [ IDENT "Eval"; r = Tactic.red_tactic; "in" ->
+	  [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ]
+      | -> [] ] ]
+  ;
+  binders_list:
+    [ [ idl = Constr.ne_binders_list -> idl
+      | -> [] ] ]
+  ;
+  gallina:
+    (* Definition, Goal *)
+    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg; "." ->
+          <:ast< (StartProof $thm $id $c) >>
+      | thm = thm_tok; id = identarg; ":"; c = constrarg; ":="; "Proof";
+        tb = theorem_body; "Qed"; "." ->
+          <:ast< (TheoremProof $thm $id $c $tb) >>
 
-  opt_identarg_list:
-  [ [ -> []
-    | ":"; l = LIST1 identarg -> l ] ]
+      | def = def_tok; s = identarg; bl = binders_list;
+	":"; t = Constr.constr; "." ->
+          <:ast< (StartProof $def $s (CONSTR ($ABSTRACT "PRODLIST" $bl $t))) >>
+      | def = def_tok; s = identarg; bl = binders_list;
+	":="; red = reduce; c = Constr.constr; "." ->
+          <:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c))
+		    ($LIST $red)) >>
+      | def = def_tok; s = identarg; bl = binders_list;
+	":="; red = reduce; c = Constr.constr; ":"; t = Constr.constr; "." ->
+          <:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c)) 
+		    (CONSTR ($ABSTRACT "PRODLIST" $bl $t)) ($LIST $red)) >>
+      | def = def_tok; s = identarg; bl = binders_list;
+	":"; t = Constr.constr; ":="; red = reduce; c = Constr.constr; "." ->
+          <:ast< (DEFINITION $def $s (CONSTR ($ABSTRACT "LAMBDALIST" $bl $c))
+		    (CONSTR ($ABSTRACT "PRODLIST" $bl $t)) ($LIST $red)) >>
+
+      | hyp = hyp_tok; bl = ne_params_list; "." ->
+          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
+      | hyp = hyps_tok; bl = ne_params_list; "." ->
+          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
+      | hyp = param_tok; bl = ne_params_list; "." ->
+          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
+      | hyp = params_tok; bl = ne_params_list; "." ->
+          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
+      ] ]
   ;
+  gallina_ext:
+      [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
+        ":="; c = constrarg; "." ->
+          <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
+      ] ];
+  END
+
+(* Gallina inductive declarations *)
+GEXTEND Gram
+  GLOBAL: gallina gallina_ext;
 
   finite_tok:
     [ [ "Inductive" -> <:ast< "Inductive" >>
       | "CoInductive" -> <:ast< "CoInductive" >> ] ]
   ;
+  record_tok:
+    [ [ IDENT "Record" -> <:ast< "Record" >>
+      | IDENT "Structure" -> <:ast< "Structure" >> ] ]
+  ;
+  constructor:
+    [ [ id = IDENT; ":"; c = Constr.constr ->
+          <:ast< (BINDER $c ($VAR $id)) >> ] ]
+  ;
+  ne_constructor_list:
+    [ [ idc = constructor; "|"; l = ne_constructor_list -> idc :: l
+      | idc = constructor -> [idc] ] ]
+  ;
+  constructor_list:
+    [ [ "|"; l = ne_constructor_list -> <:ast< (BINDERLIST ($LIST $l)) >>
+      | l = ne_constructor_list -> <:ast< (BINDERLIST ($LIST $l)) >>
+      |  -> <:ast< (BINDERLIST) >> ] ]
+  ;
   block_old_style:
     [ [ ind = oneind_old_style; "with"; indl = block_old_style -> ind :: indl
       | ind = oneind_old_style -> [ind] ] ]
   ;
   oneind_old_style:
-    [ [ id = identarg; ":"; c = comarg; ":="; lidcom = lidcom ->
-          <:ast< (VERNACARGLIST $id $c $lidcom) >> ] ]
+    [ [ id = identarg; ":"; c = constrarg; ":="; lc = constructor_list ->
+          <:ast< (VERNACARGLIST $id $c $lc) >> ] ]
   ;
   block:
     [ [ ind = oneind; "with"; indl = block -> ind :: indl
       | ind = oneind -> [ind] ] ]
   ;
   oneind:
-    [ [ id = identarg; indpar = indpar; ":"; c = comarg; ":="; lidcom = lidcom
-      -> <:ast< (VERNACARGLIST $id $c $indpar $lidcom) >> ] ]
+    [ [ id = identarg; indpar = indpar; ":"; c = constrarg; ":=";
+	lc = constructor_list
+      -> <:ast< (VERNACARGLIST $id $c $indpar $lc) >> ] ]
+  ;
+  indpar:
+    [ [ bl = ne_simple_binders_list ->
+          <:ast< (BINDERLIST ($LIST $bl)) >>
+      |  -> <:ast< (BINDERLIST) >> ] ]
+  ;
+  opt_coercion:
+    [ [ ">" -> "COERCION"
+      |  -> "" ] ]
+  ;
+  onescheme:
+    [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
+        s = sortarg ->
+          <:ast< (VERNACARGLIST $id $dep $indid $s) >> ] ]
+  ;
+  specifscheme:
+    [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl
+      | rec_ = onescheme -> [rec_] ] ]
+  ;
+  dep:
+    [ [ IDENT "Induction"; IDENT "for" -> <:ast< "DEP" >>
+      | IDENT "Minimality"; IDENT "for" -> <:ast< "NODEP" >> ] ]
   ;
   onerec:
-    [ [ id = identarg; "["; idl = ne_binder_list; "]"; ":"; c = comarg;
-        ":="; def = comarg ->
+    [ [ id = identarg; idl = ne_simple_binders_list; ":"; c = constrarg;
+        ":="; def = constrarg ->
           <:ast< (VERNACARGLIST $id (BINDERLIST ($LIST $idl)) $c $def) >> ] ]
   ;
   specifrec:
@@ -81,26 +198,18 @@ GEXTEND Gram
       | rec_ = onerec -> [rec_] ] ]
   ;
   onecorec:
-    [ [ id = identarg; ":"; c = comarg; ":="; def = comarg ->
+    [ [ id = identarg; ":"; c = constrarg; ":="; def = constrarg ->
           <:ast< (VERNACARGLIST $id $c $def) >> ] ]
   ;
   specifcorec:
     [ [ corec = onecorec; "with"; corecl = specifcorec -> corec :: corecl
       | corec = onecorec -> [corec] ] ]
   ;
-  rec_constr:
-    [ [ c = Vernac.identarg -> <:ast< (VERNACARGLIST $c) >>
-      |  -> <:ast< (VERNACARGLIST) >> ] ]
-  ;
-  record_tok:
-    [ [ IDENT "Record" -> <:ast< "Record" >>
-      | IDENT "Structure" -> <:ast< "Structure" >> ] ]
-  ;
   field:
-    [ [ id = identarg; ":"; c = Constr.constr ->
-          <:ast< (VERNACARGLIST "" $id (CONSTR $c)) >>
-      | id = identarg; ":>"; c = Constr.constr ->
-          <:ast< (VERNACARGLIST "COERCION" $id (CONSTR $c)) >> ] ]
+    [ [ id = identarg; ":"; oc = opt_coercion; c = constrarg ->
+          <:ast< (VERNACARGLIST ($STR $oc) $id $c) >>
+(*      | id = identarg; ":>"; c = constrarg ->
+          <:ast< (VERNACARGLIST "COERCION" $id $c) >> *)] ]
   ;
   nefields:
     [ [ idc = field; ";"; fs = nefields -> idc :: fs
@@ -110,178 +219,42 @@ GEXTEND Gram
     [ [ fs = nefields -> <:ast< (VERNACARGLIST ($LIST $fs)) >>
       |  -> <:ast< (VERNACARGLIST) >> ] ]
   ;
-  onescheme:
-    [ [ id = identarg; ":="; dep = dep; indid = identarg; IDENT "Sort";
-        s = sortdef ->
-          <:ast< (VERNACARGLIST $id $dep $indid (CONSTR $s)) >> ] ]
-  ;
-  specifscheme:
-    [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl
-      | rec_ = onescheme -> [rec_] ] ]
-  ;
-  dep:
-    [ [ IDENT "Induction"; IDENT "for" -> <:ast< "DEP" >>
-      | IDENT "Minimality"; IDENT "for" -> <:ast< "NODEP" >> ] ]
-  ;
-  ne_binder_list:
-    [ [ id = binder; ";"; idl = ne_binder_list -> id :: idl
-      | id = binder -> [id] ] ]
-  ;
-  indpar:
-    [ [ "["; bl = ne_binder_list; "]" ->
-          <:ast< (BINDERLIST ($LIST $bl)) >>
-      |  -> <:ast< (BINDERLIST) >> ] ]
-  ;
-  sortdef:
-    [ [ "Set"  -> <:ast< (SET) >>
-      | "Prop" -> <:ast< (PROP) >>
-      | "Type" -> <:ast< (TYPE) >> ] ]
-  ;
-  thm_tok:
-    [ [ "Theorem" -> <:ast< "THEOREM" >>
-      | IDENT "Lemma" -> <:ast< "LEMMA" >>
-      | IDENT "Fact" -> <:ast< "FACT" >>
-      | IDENT "Remark" -> <:ast< "REMARK" >> ] ]
-  ;
-
-  def_tok:
-    [ [ "Definition" -> <:ast< "DEFINITION" >>
-      | IDENT "Local" -> <:ast< "LOCAL" >> 
-      | "@"; "Definition"  -> <:ast< "OBJECT" >>
-      | "@"; IDENT "Local"  -> <:ast< "LOBJECT" >>
-      | "@"; IDENT "Coercion"  -> <:ast< "OBJCOERCION" >>
-      | "@"; IDENT "Local"; IDENT "Coercion"  -> <:ast< "LOBJCOERCION" >>
-      | IDENT "SubClass"  -> <:ast< "SUBCLASS" >>
-      | IDENT "Local"; IDENT "SubClass"  -> <:ast< "LSUBCLASS" >> ] ]  
-  ;
-  import_tok:
-    [ [ IDENT "Import" -> <:ast< "IMPORT" >>
-      | IDENT "Export" -> <:ast< "EXPORT" >>
-      |  -> <:ast< "IMPORT" >> ] ]
-  ;
-  specif_tok:
-    [ [ IDENT "Implementation" -> <:ast< "IMPLEMENTATION" >>
-      | IDENT "Specification" -> <:ast< "SPECIFICATION" >>
-      |  -> <:ast< "UNSPECIFIED" >> ] ]
-  ;
-  hyp_tok:
-    [ [ "Hypothesis" -> <:ast< "HYPOTHESIS" >>
-      | "Variable" -> <:ast< "VARIABLE" >> ] ]
-  ;
-  hyps_tok:
-    [ [ IDENT "Hypotheses" -> <:ast< "HYPOTHESES" >>
-      | IDENT "Variables" -> <:ast< "VARIABLES" >> ] ]
-  ;
-  param_tok:
-    [ [ "Axiom" -> <:ast< "AXIOM" >>
-      | "Parameter" -> <:ast< "PARAMETER" >> ] ]
-  ;
-  params_tok:
-    [ [ IDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ]
+  simple_params:
+    [ [ idl = Constr.ne_ident_comma_list; ":"; c = Constr.constr ->
+          <:ast< (BINDER $c ($LIST $idl)) >>
+      | idl = Constr.ne_ident_comma_list ->
+          <:ast< (BINDER (ISEVAR) ($LIST $idl)) >> ] ]
   ;
-  binder:
-    [ [ idl = ne_identarg_comma_list; ":"; c = Constr.constr ->
-          <:ast< (BINDER $c ($LIST $idl)) >> ] ]
+  ne_simple_params_list:
+    [ [ id = simple_params; ";"; idl = ne_simple_params_list -> id :: idl
+      | id = simple_params -> [id] ] ]
   ;
-  idcom:
-    [ [ id = IDENT; ":"; c = Constr.constr ->
-          <:ast< (BINDER $c ($VAR $id)) >> ] ]
+  simple_binders:
+    [ [ "["; bl = ne_simple_params_list; "]" -> bl ] ]
   ;
-  ne_lidcom:
-    [ [ idc = idcom; "|"; l = ne_lidcom -> idc :: l
-      | idc = idcom -> [idc] ] ]
+  ne_simple_binders_list:
+    [ [ bl = simple_binders; bll = ne_simple_binders_list -> bl @ bll
+      | bl = simple_binders -> bl ] ]
   ;
-  lidcom:
-    [ [ l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >>
-      | "|"; l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >>
-      |  -> <:ast< (BINDERLIST) >> ] ]
+  rec_constr:
+    [ [ c = Vernac.identarg -> <:ast< (VERNACARGLIST $c) >>
+      |  -> <:ast< (VERNACARGLIST) >> ] ]
   ;
-  END
-
-GEXTEND Gram
-  vernac:
-      (* Definition, Goal *)
-    [ [ thm = thm_tok; id = identarg; ":"; c = comarg; "." ->
-          <:ast< (StartProof $thm $id $c) >>
-      | thm = thm_tok; id = identarg; ":"; c = comarg; ":="; "Proof";
-        tb = theorem_body; "Qed"; "." ->
-          <:ast< (TheoremProof $thm $id $c $tb) >>
-
-      | def = def_tok; s = identarg; ":"; c1 = Constr.constr; "." ->
-          <:ast< (StartProof $def $s (CONSTR $c1)) >>
-      | def = def_tok; s = identarg; ":="; c1 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s (CONSTR $c1)) >>
-      | def = def_tok; s = identarg; ":="; c1 = Constr.constr; ":";
-        c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s (CONSTR (CAST $c1 $c2))) >>
-      | def = def_tok; s = identarg; ":"; c1 = Constr.constr; ":=";
-        c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s (CONSTR (CAST $c2 $c1))) >>
-
-(* CP / Juillet 99 
-   Ajout de la possibilite d'appliquer une regle de reduction au 
-   corps d'une definition 
-   Definition t := Eval red in term
-*)
-
-      | def = def_tok; s = identarg; ":="; 
-      IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s (CONSTR $c1) (TACTIC_ARG (REDEXP $r))) >>
-      | def = def_tok; s = identarg; ":="; 
-      IDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Constr.constr; ":";
-        c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s 
-                 (CONSTR (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >>
-      | def = def_tok; s = identarg; ":"; c1 = Constr.constr; ":=";
-        IDENT "Eval"; r = Tactic.red_tactic; "in"; 
-	c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION $def $s (CONSTR (CAST $c2 $c1)) 
-		    (TACTIC_ARG (REDEXP $r))) >>
-
-(* Papageno / Février 99
-   Ajout du racourci "Definition x [c:nat] := t" pour 
-                     "Definition x := [c:nat]t" *)
-
-      | def = def_tok; s = identarg; "["; id1 = IDENT; ":"; 
-	c = Constr.constr; t = definition_tail;  "." -> 
-	  <:ast< (DEFINITION $def $s (CONSTR (LAMBDA $c [$id1]$t))) >>
-
-      | def = def_tok; s = identarg; "["; id1 = IDENT; ",";
-	idl = Constr.ne_ident_comma_list; ":"; c = Constr.constr; 
-	t = definition_tail; "." -> 
-	  <:ast< (DEFINITION $def $s (CONSTR 
-			(LAMBDALIST $c [$id1]($SLAM $idl $t)))) >>
-
-
-      | hyp = hyp_tok; bl = ne_binder_list; "." ->
-          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
-      | hyp = hyps_tok; bl = ne_binder_list; "." ->
-          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
-      | hyp = param_tok; bl = ne_binder_list; "." ->
-          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
-      | hyp = params_tok; bl = ne_binder_list; "." ->
-          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
-      | IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
-        ":="; c = comarg; "." ->
-          <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
-      | f = finite_tok; s = sortdef; id = identarg; indpar = indpar; ":=";
-        lidcom = lidcom; "." ->
-          <:ast< (ONEINDUCTIVE $f $id (CONSTR $s) $indpar $lidcom) >>
-      | f = finite_tok; indl = block; "." ->
-          <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
-
-      | record_tok; name = identarg; ps = indpar; ":"; s = sortdef; ":=";
-        c = rec_constr; "{"; fs = fields; "}"; "." ->
-          <:ast< (RECORD "" $name $ps (CONSTR $s) $c $fs) >>
-      | record_tok; ">"; name = identarg; ps = indpar; ":"; s = sortdef; ":=";
-        c = rec_constr; "{"; fs = fields; "}"; "." ->
-          <:ast< (RECORD "COERCION" $name $ps (CONSTR $s) $c $fs) >>
-
-      | IDENT "Mutual"; "["; bl = ne_binder_list; "]" ; f = finite_tok;
+  gallina_ext:
+    [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_tok;
         indl = block_old_style; "." ->
           <:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
                                      (VERNACARGLIST ($LIST $indl))) >>
-      | IDENT "Mutual"; f = finite_tok; indl = block; "." ->
+      | record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+          <:ast< (RECORD ($STR $oc) $name $ps $s $c $fs) >>
+(*      | record_tok; ">"; name = identarg; ps = indpar; ":";
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+          <:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
+*)      ] ]
+  ;
+  gallina:
+    [ [ IDENT "Mutual"; f = finite_tok; indl = block; "." ->
           <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
       | "Fixpoint"; recs = specifrec; "." ->
           <:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >>
@@ -289,22 +262,98 @@ GEXTEND Gram
           <:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >>
       | IDENT "Scheme"; schemes = specifscheme; "." ->
           <:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >>
-      ] ];
+      | f = finite_tok; s = sortarg; id = identarg; indpar = indpar; ":=";
+        lc = constructor_list; "." ->
+          <:ast< (ONEINDUCTIVE $f $id $s $indpar $lc) >>
+      | f = finite_tok; indl = block; "." ->
+          <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
 
-      
-      definition_tail:
-    	[ [ ";"; idl = Constr.ne_ident_comma_list;
-            ":"; c = Constr.constr; c2 = definition_tail ->
-              <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >>
-	| "]"; ":"; ty = Constr.constr; ":=" ; c = Constr.constr -> 
-	    <:ast< (CAST $c $ty) >>
- 	| "]"; ":="; c = Constr.constr -> c 
-	] ];
+      | record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+          <:ast< (RECORD ($STR $oc) $name $ps $s $c $fs) >>
+(*      | record_tok; ">"; name = identarg; ps = indpar; ":";
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+          <:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
+*)      ] ];
 
   END
 
 GEXTEND Gram
-  vernac:
+  GLOBAL: gallina_ext;
+
+  gallina_ext:
+    [ [ 
+
+(* Sections *)
+	IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+      | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+      | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
+      | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
+
+(* Transparent and Opaque *)
+      | IDENT "Transparent"; l = ne_identarg_list; "." ->
+          <:ast< (TRANSPARENT ($LIST $l)) >>
+      | IDENT "Opaque"; l = ne_identarg_list; "." -> 
+	  <:ast< (OPAQUE ($LIST $l)) >>
+
+(* Coercions *)
+      | IDENT "Coercion"; s = identarg; ":="; c = Constr.constr; "." ->
+          <:ast< (DEFINITION "COERCION" $s (CONSTR $c)) >>
+      | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; ":";
+         c2 = Constr.constr; "." ->
+          <:ast< (DEFINITION "COERCION" $s (CONSTR (CAST $c1 $c2))) >>
+      | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
+	 c = constrarg; "." ->
+          <:ast< (DEFINITION "LCOERCION" $s $c) >>
+      | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
+	 c1 = Constr.constr; ":"; c2 = Constr.constr; "." ->
+          <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
+      | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identarg;
+         ":"; c = identarg; ">->"; d = identarg; "." ->
+          <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
+      | IDENT "Identity"; IDENT "Coercion"; f = identarg; ":";
+         c = identarg; ">->"; d = identarg; "." ->
+          <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
+      | IDENT "Coercion"; IDENT "Local"; f = identarg; ":"; c = identarg;
+        ">->"; d = identarg; "." ->
+          <:ast< (COERCION "LOCAL" "" $f $c $d) >>
+      | IDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
+         d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
+      | IDENT "Class"; IDENT "Local"; c = identarg; "." ->
+          <:ast< (CLASS "LOCAL" $c) >>
+      | IDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
+
+(* Implicit *)
+      | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg;
+         "." -> <:ast< (SyntaxMacro $id $com) >>
+      | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg;
+         "|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >>
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "On"; "." ->
+          <:ast< (IMPLICIT_ARGS_ON) >>
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off"; "." ->
+          <:ast< (IMPLICIT_ARGS_OFF) >>
+      | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
+          <:ast< (IMPLICITS "" $id ($LIST $l)) >>
+      | IDENT "Implicits"; id = identarg; "." ->
+          <:ast< (IMPLICITS "Auto" $id) >> 
+  ] ]
+  ;
+END
+
+GEXTEND Gram
+  GLOBAL: command;
+
+  import_tok:
+    [ [ IDENT "Import" -> <:ast< "IMPORT" >>
+      | IDENT "Export" -> <:ast< "EXPORT" >>
+      |  -> <:ast< "IMPORT" >> ] ]
+  ;
+  specif_tok:
+    [ [ IDENT "Implementation" -> <:ast< "IMPLEMENTATION" >>
+      | IDENT "Specification" -> <:ast< "SPECIFICATION" >>
+      |  -> <:ast< "UNSPECIFIED" >> ] ]
+  ;
+  command:
     [ [ 
 
 (* State management *)
@@ -321,8 +370,23 @@ GEXTEND Gram
       | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
           <:ast< (ResetSection $id) >>
 
-(* Modules and Sections *)   
-
+(* Modules management *)   
+      | "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
+	s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
+          <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
+      | "Compile";
+	verbosely =
+          [ IDENT "Verbose" -> "Verbose"
+          | -> "" ];
+	IDENT "Module";
+	only_spec =
+          [ IDENT "Specification" -> "Specification"
+          | -> "" ];
+	mname = [ s = STRING -> s | s = IDENT -> s ];
+	fname = OPT [ s = STRING -> s | s = IDENT -> s ]; "." ->
+          let fname = match fname with Some s -> s | None -> mname in
+            <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
+                      ($STR $mname) ($STR $fname))>>
       | IDENT "Read"; IDENT "Module"; id = identarg; "." ->
           <:ast< (ReadModule $id) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
@@ -330,80 +394,39 @@ GEXTEND Gram
       | IDENT "Require"; import = import_tok; specif = specif_tok;
         id = identarg; filename = stringarg; "." ->
           <:ast< (RequireFrom $import $specif $id $filename) >>
-      | IDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
-      | IDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
-      | IDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
       | IDENT "Write"; IDENT "Module"; id = identarg; "." -> 
 	  <:ast< (WriteModule $id) >>
       | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg; "." -> 
 	  <:ast< (WriteModule $id $s) >>
       | IDENT "Begin"; IDENT "Silent"; "." -> <:ast< (BeginSilent) >>
       | IDENT "End"; IDENT "Silent"; "." -> <:ast< (EndSilent) >>
-      | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
       | IDENT "Declare"; IDENT "ML"; IDENT "Module";
         l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
       | IDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
-	  (* Transparent and Opaque *)
-      | IDENT "Transparent"; l = ne_identarg_list; "." ->
-          <:ast< (TRANSPARENT ($LIST $l)) >>
-      | IDENT "Opaque"; l = ne_identarg_list; "." -> 
-	  <:ast< (OPAQUE ($LIST $l)) >>
       
-	  (* Extraction *)
+(* Extraction *)
       | IDENT "Extraction"; id = identarg; "." ->
           <:ast< (PrintExtractId $id) >>
       | IDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
 
-(* Grammar extensions, Coercions, Implicits *)
-	  
-     | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; "." ->
-         <:ast< (DEFINITION "COERCION" $s (CONSTR $c1)) >>
-     | IDENT "Coercion"; s = identarg; ":="; c1 = Constr.constr; ":";
-        c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION "COERCION" $s (CONSTR (CAST $c1 $c2))) >>
-     | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
-	c1 = Constr.constr; "." ->
-          <:ast< (DEFINITION "LCOERCION" $s (CONSTR $c1)) >>
-     | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
-	c1 = Constr.constr; ":"; c2 = Constr.constr; "." ->
-          <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
-	  
-	  
-     | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
-        "." -> <:ast< (SyntaxMacro $id $com) >>
-     | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
-        "|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >>
-     | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
-         <:ast< (PrintGrammar $uni $ent) >>
-     | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identarg;
-        ":"; c = identarg; ">->"; d = identarg; "." ->
-          <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
-     | IDENT "Identity"; IDENT "Coercion"; f = identarg; ":";
-        c = identarg; ">->"; d = identarg; "." ->
-          <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
-     | IDENT "Coercion"; IDENT "Local"; f = identarg; ":"; c = identarg;
-        ">->"; d = identarg; "." ->
-          <:ast< (COERCION "LOCAL" "" $f $c $d) >>
-     | IDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
-        d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
-     | IDENT "Class"; IDENT "Local"; c = identarg; "." ->
-         <:ast< (CLASS "LOCAL" $c) >>
-     | IDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
-     | IDENT "Implicit"; IDENT "Arguments"; IDENT "On"; "." ->
-         <:ast< (IMPLICIT_ARGS_ON) >>
-     | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off"; "." ->
-         <:ast< (IMPLICIT_ARGS_OFF) >>
-     | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
-         <:ast< (IMPLICITS "" $id ($LIST $l)) >>
-     | IDENT "Implicits"; id = identarg; "." ->
-         <:ast< (IMPLICITS "Auto" $id) >> 
  ] ];
     END
 
-(* Proof constrs *)
+(* Proof commands *)
 GEXTEND Gram
-  vernac:
-    [ [ IDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >>
+  GLOBAL: command;
+
+  destruct_location :
+  [ [ IDENT "Conclusion"  -> <:ast< (CONCL)>>
+    | IDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
+    | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
+  ;
+  opt_identarg_list:
+  [ [ -> []
+    | ":"; l = LIST1 identarg -> l ] ]
+  ;
+  command:
+    [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
       | IDENT "Goal"; "." -> <:ast< (GOAL) >>
       | "Proof"; "." -> <:ast< (GOAL) >>
       | IDENT "Abort"; "." -> <:ast< (ABORT) >>
@@ -421,7 +444,7 @@ GEXTEND Gram
       | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
       | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
       | IDENT "Restart"; "." -> <:ast< (RESTART) >>
-      | "Proof"; c = comarg; "." -> <:ast< (PROOF $c) >>
+      | "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >>
       | IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
       | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
       | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
@@ -435,8 +458,8 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
       | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
       | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
-      | IDENT "Existential"; n = numarg; ":="; c = Constr.constr; "." ->
-          <:ast< (EXISTENTIAL $n (CONSTR $c)) >>
+      | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
+          <:ast< (EXISTENTIAL $n $c) >>
       | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
         c2 = Constr.constr; "." ->
           <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
@@ -467,11 +490,11 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
 
       | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
-	IDENT "Resolve"; c = comarg; "." ->
+	IDENT "Resolve"; c = constrarg; "." ->
 	  <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Immediate"; c = comarg; "." ->
+	IDENT "Immediate"; c = constrarg; "." ->
 	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
@@ -483,7 +506,7 @@ GEXTEND Gram
 	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Extern"; n = numarg; c = comarg ; tac = tacarg; "." ->
+	IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
 	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
 		   $n $c (TACTIC $tac))>>
 	  
@@ -502,7 +525,7 @@ GEXTEND Gram
       | IDENT "HintDestruct"; 
                 dloc = destruct_location;
                 na  = identarg;
-                hyptyp = comarg;
+                hyptyp = constrarg;
                 pri = numarg;
                 tac = Prim.astact; "." -> 
           <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
@@ -511,7 +534,7 @@ GEXTEND Gram
           <:ast< (SOLVE $n (TACTIC $tac)) >> 
 
 (*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; com = comarg; "." ->
+      | IDENT "PrintConstr"; com = constrarg; "." ->
           <:ast< (PrintConstr $com)>>
       ] ];
   END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6da37473f4..54fd236b66 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -123,11 +123,29 @@ let map_entry f en =
 let parse_string f x =
   let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
 
-let slam_ast loc id ast =
+let slam_ast (_,fin) id ast =
   match id with
-    | Coqast.Nvar (_, s) -> Coqast.Slam (loc, Some s, ast)
+    | Coqast.Nvar ((deb,_), s) -> Coqast.Slam ((deb,fin), Some s, ast)
     | _ -> invalid_arg "Ast.slam_ast"
 
+(* This is to interpret the macro $ABSTRACT used in binders        *)
+(* $ABSTRACT should occur in this configuration :                  *)
+(* ($ABSTRACT name (s1 a1 ($LIST l1)) ... (s2 an ($LIST ln)) b)    *)
+(* where li is id11::...::id1p1 and it produces the ast            *)
+(* (s1' a1 [id11]...[id1p1](... (sn' an [idn1]...[idnpn]b)...))    *)
+(* where s1' is overwritten by name if s1 is $BINDER otherwise s1  *)
+
+let abstract_binder_ast (_,fin as loc) name a b =
+  match a with
+    | Coqast.Node((deb,_),s,d::l) ->
+	let s' = if s="$BINDER" then name else s in
+	Coqast.Node((deb,fin),s', [d; List.fold_right (slam_ast loc) l b])
+    | _ -> invalid_arg "Bad usage of $ABSTRACT macro"
+
+let abstract_binders_ast loc name =
+  List.fold_right (abstract_binder_ast loc name)
+
+
 type entry_type = ETast | ETastl
     
 let entry_type ast =
@@ -211,7 +229,7 @@ module Constr =
     let gec s =
       let e = Gram.Entry.create ("Constr." ^ s) in
       Hashtbl.add uconstr s (Ast e); e
-	
+
     let gec_list s =
       let e = Gram.Entry.create ("Constr." ^ s) in
       Hashtbl.add uconstr s (ListAst e); e
@@ -234,24 +252,10 @@ module Constr =
     let ident = gec "ident"
     let ne_ident_comma_list = gec_list "ne_ident_comma_list"
     let ne_constr_list = gec_list "ne_constr_list"
-
+    let sort = gec "sort"
     let pattern = Gram.Entry.create "Constr.pattern"
+    let ne_binders_list = gec_list "ne_binders_list"
 
-(*
-    let binder = gec "binder"
-
-    let abstraction_tail = gec "abstraction_tail"
-    let cofixbinder = gec "cofixbinder"
-    let cofixbinders = gec_list "cofixbinders"
-    let fixbinder = gec "fixbinder"
-    let fixbinders = gec_list "fixbinders"
-
-    let ne_binder_list = gec_list "ne_binder_list"
-
-    let ne_pattern_list = Gram.Entry.create "Constr.ne_pattern_list"
-    let pattern_list = Gram.Entry.create "Constr.pattern_list"
-    let simple_pattern = Gram.Entry.create "Constr.simple_pattern"
-*)
     let uconstr = snd (get_univ "constr")
   end
 
@@ -323,68 +327,21 @@ module Vernac =
       let e = Gram.Entry.create ("Vernac." ^ s) in
       Hashtbl.add uvernac s (ListAst e); e
     
-    let binder = gec "binder"
-    let block = gec_list "block"
-    let block_old_style = gec_list "block_old_style"
-    let comarg = gec "comarg"
-    let def_tok = gec "def_tok"
-    let definition_tail  = gec "definition_tail"
-    let dep = gec "dep"
-    let destruct_location = gec "destruct_location"
-    let check_tok = gec "check_tok"
-    let extracoindblock = gec_list "extracoindblock"
-    let extraindblock = gec_list "extraindblock"
-    let field = gec "field"
-    let nefields = gec_list "nefields"
-    let fields = gec "fields"
-    let destruct_location = gec "destruct_location"
-    let finite_tok = gec "finite_tok"
-    let grammar_entry_arg = gec "grammar_entry_arg"
-    let hyp_tok = gec "hyp_tok"
-    let hyps_tok = gec "hyps_tok"
-    let idcom = gec "idcom"
     let identarg = gec "identarg"
-    let import_tok = gec "import_tok"
-    let indpar = gec "indpar"
-    let lcomarg = gec "lcomarg"
-    let lidcom = gec "lidcom"
-    let orient=gec "orient"
-    let lvernac = gec_list "lvernac"
-    let meta_binding = gec "meta_binding"
-    let meta_binding_list = gec_list "meta_binding_list"
-    let ne_binder_list = gec_list "ne_binder_list"
-    let ne_comarg_list = gec_list "ne_comarg_list"
-    let ne_identarg_comma_list = gec_list "ne_identarg_comma_list"
-    let identarg_list = gec_list "identarg_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
-    let ne_lidcom = gec_list "ne_lidcom"
-    let ne_numarg_list = gec_list "ne_numarg_list"
-    let ne_stringarg_list = gec_list "ne_stringarg_list"
     let numarg = gec "numarg"
     let numarg_list = gec_list "numarg_list"
-    let onecorec = gec "onecorec"
-    let oneind = gec "oneind"
-    let oneind_old_style = gec "oneind_old_style"
-    let onerec = gec "onerec"
-    let onescheme = gec "onescheme"
-    let opt_identarg_list = gec_list "opt_identarg_list"
-    let rec_constr = gec "rec_constr"
-    let record_tok = gec "record_tok"
-    let option_value = gec "option_value"
-    let param_tok = gec "param_tok"
-    let params_tok = gec "params_tok"
-    let sortdef = gec "sortdef"
-    let specif_tok = gec "specif_tok"
-    let specifcorec = gec_list "specifcorec"
-    let specifrec = gec_list "specifrec"
-    let specifscheme = gec_list "specifscheme"
+    let ne_numarg_list = gec_list "ne_numarg_list"
     let stringarg = gec "stringarg"
+    let ne_stringarg_list = gec_list "ne_stringarg_list"
+    let constrarg = gec "constrarg"
     let tacarg = gec "tacarg"
-    let theorem_body = gec "theorem_body"
-    let theorem_body_line = gec "theorem_body_line"
-    let theorem_body_line_list = gec_list "theorem_body_line_list"
-    let thm_tok = gec "thm_tok"
-    let varg_ne_stringarg_list = gec "varg_ne_stringarg_list"
+    let sortarg = gec "sortarg"
+
+    let gallina = gec "gallina"
+    let gallina_ext = gec "gallina_ext"
+    let command = gec "command"
+    let syntax_command = gec "syntax_command"
     let vernac = gec "vernac"
     let vernac_eoi = eoi_entry vernac
   end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8bc7642e36..cc868939d0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -26,6 +26,8 @@ val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
 val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
 
 val slam_ast : Coqast.loc -> Coqast.t -> Coqast.t -> Coqast.t
+val abstract_binders_ast :
+  Coqast.loc -> string -> Coqast.t list -> Coqast.t -> Coqast.t
 
 (* Entry types *)
 
@@ -76,24 +78,9 @@ module Constr :
     val ident : Coqast.t Gram.Entry.e
     val ne_ident_comma_list : Coqast.t list Gram.Entry.e
     val ne_constr_list : Coqast.t list Gram.Entry.e
-
+    val sort : Coqast.t Gram.Entry.e
     val pattern : Coqast.t Gram.Entry.e
-
-(*
-    val binder : Coqast.t Gram.Entry.e
-
-    val abstraction_tail : Coqast.t Gram.Entry.e
-    val cofixbinder : Coqast.t Gram.Entry.e
-    val cofixbinders : Coqast.t list Gram.Entry.e
-    val fixbinder : Coqast.t Gram.Entry.e
-    val fixbinders : Coqast.t list Gram.Entry.e
-
-    val ne_binder_list : Coqast.t list Gram.Entry.e
-
-    val ne_pattern_list : Coqast.t list Gram.Entry.e
-    val pattern_list : Coqast.t list Gram.Entry.e
-    val simple_pattern : Coqast.t Gram.Entry.e
-*)
+    val ne_binders_list : Coqast.t list Gram.Entry.e
   end
 
 module Tactic :
@@ -143,66 +130,21 @@ module Tactic :
 
 module Vernac :
   sig
-    val binder : Coqast.t Gram.Entry.e
-    val block : Coqast.t list Gram.Entry.e
-    val block_old_style : Coqast.t list Gram.Entry.e
-    val check_tok : Coqast.t Gram.Entry.e
-    val comarg : Coqast.t Gram.Entry.e
-    val def_tok : Coqast.t Gram.Entry.e
-    val definition_tail : Coqast.t Gram.Entry.e
-    val dep : Coqast.t Gram.Entry.e
-    val destruct_location : Coqast.t Gram.Entry.e
-    val destruct_location : Coqast.t Gram.Entry.e
-    val extracoindblock : Coqast.t list Gram.Entry.e
-    val extraindblock : Coqast.t list Gram.Entry.e
-    val field : Coqast.t Gram.Entry.e
-    val fields : Coqast.t Gram.Entry.e
-    val finite_tok : Coqast.t Gram.Entry.e
-    val hyp_tok : Coqast.t Gram.Entry.e
-    val hyps_tok : Coqast.t Gram.Entry.e
-    val idcom : Coqast.t Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
-    val import_tok : Coqast.t Gram.Entry.e
-    val indpar : Coqast.t Gram.Entry.e
-    val lcomarg : Coqast.t Gram.Entry.e
-    val lidcom : Coqast.t Gram.Entry.e
-    val orient:Coqast.t Gram.Entry.e;; 
-    val lvernac : Coqast.t list Gram.Entry.e
-    val meta_binding : Coqast.t Gram.Entry.e
-    val meta_binding_list : Coqast.t list Gram.Entry.e
-    val ne_binder_list : Coqast.t list Gram.Entry.e
-    val ne_comarg_list : Coqast.t list Gram.Entry.e
-    val ne_identarg_comma_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
-    val ne_lidcom : Coqast.t list Gram.Entry.e
-    val ne_numarg_list : Coqast.t list Gram.Entry.e
-    val ne_stringarg_list : Coqast.t list Gram.Entry.e
-    val nefields : Coqast.t list Gram.Entry.e
     val numarg : Coqast.t Gram.Entry.e
     val numarg_list : Coqast.t list Gram.Entry.e
-    val onecorec : Coqast.t Gram.Entry.e
-    val oneind : Coqast.t Gram.Entry.e
-    val oneind_old_style : Coqast.t Gram.Entry.e
-    val onerec : Coqast.t Gram.Entry.e
-    val onescheme : Coqast.t Gram.Entry.e
-    val opt_identarg_list : Coqast.t list Gram.Entry.e
-    val option_value : Coqast.t Gram.Entry.e
-    val param_tok : Coqast.t Gram.Entry.e
-    val params_tok : Coqast.t Gram.Entry.e
-    val rec_constr : Coqast.t Gram.Entry.e
-    val record_tok : Coqast.t Gram.Entry.e
-    val sortdef : Coqast.t Gram.Entry.e
-    val specif_tok : Coqast.t Gram.Entry.e
-    val specifcorec : Coqast.t list Gram.Entry.e
-    val specifrec : Coqast.t list Gram.Entry.e
-    val specifscheme : Coqast.t list Gram.Entry.e
+    val ne_numarg_list : Coqast.t list Gram.Entry.e
     val stringarg : Coqast.t Gram.Entry.e
+    val ne_stringarg_list : Coqast.t list Gram.Entry.e
+    val constrarg : Coqast.t Gram.Entry.e
     val tacarg : Coqast.t Gram.Entry.e
-    val theorem_body : Coqast.t Gram.Entry.e
-    val theorem_body_line : Coqast.t Gram.Entry.e
-    val theorem_body_line_list : Coqast.t list Gram.Entry.e
-    val thm_tok : Coqast.t Gram.Entry.e
-    val varg_ne_stringarg_list : Coqast.t Gram.Entry.e
+    val sortarg : Coqast.t Gram.Entry.e
+
+    val gallina : Coqast.t Gram.Entry.e
+    val gallina_ext : Coqast.t Gram.Entry.e
+    val command : Coqast.t Gram.Entry.e
+    val syntax_command : Coqast.t Gram.Entry.e
     val vernac : Coqast.t Gram.Entry.e
     val vernac_eoi : Coqast.t Gram.Entry.e
   end
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index ae8d8bfd39..9272132802 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -24,6 +24,10 @@ let anti loc x =
   in
   <:expr< $anti:e$ >>
 
+(* [expr_of_ast] contributes to translate g_*.ml4 files into g_*.ppo *)
+(* This is where $id's (and macros) in ast are translated in ML variables *)
+(* which will bind their actual ast value *)
+
 let rec expr_of_ast = function
   | Coqast.Nvar loc id when is_meta id -> anti loc id
   | Coqast.Id loc id when is_meta id -> anti loc id
@@ -35,7 +39,10 @@ let rec expr_of_ast = function
       <:expr< Coqast.Str loc $anti loc x$ >>
   | Coqast.Node _ "$SLAM" [Coqast.Nvar loc idl; y] ->
       <:expr<
-        List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $expr_of_ast y$ >>
+      List.fold_right (Pcoq.slam_ast loc) $anti loc idl$ $expr_of_ast y$ >>
+  | Coqast.Node _ "$ABSTRACT" [Coqast.Str _ s;Coqast.Nvar loc idl; y] ->
+      <:expr<
+      Pcoq.abstract_binders_ast loc $str:s$ $anti loc idl$ $expr_of_ast y$ >>
   | Coqast.Node loc nn al ->
       let e = expr_list_of_ast_list al in
       <:expr< Coqast.Node loc $str:nn$ $e$ >>
@@ -60,7 +67,9 @@ and expr_list_of_ast_list al =
        | (Coqast.Node _ "$LIST" [Coqast.Nvar locv pv]) ->
            let e1 = anti locv pv in
            let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
-           <:expr< ( $lid:"@"$ $e1$ $e2$) >>
+	     if e2 = (let loc = dummy_loc in <:expr< [] >>)
+	     then <:expr< $e1$ >>
+	     else <:expr< ( $lid:"@"$ $e1$ $e2$) >>
        | _ ->
            let e1 = expr_of_ast a in
            let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e62e85d57d..1d20f928a3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -28,21 +28,11 @@ let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
 (* 1| Constant definitions *)
 
-let constant_entry_of_com com =
+let constant_entry_of_com (com,comtypopt) =
   let sigma = Evd.empty in
   let env = Global.env() in
-  match com with
-    | Node(_,"CAST",[_;t]) ->
-        { const_entry_body = Cooked (constr_of_com sigma env com);
-	  const_entry_type = Some (constr_of_com1 true sigma env t) }
-    | _ -> 
-	{ const_entry_body = Cooked (constr_of_com sigma env com);
-	  const_entry_type = None }
-
-let definition_body ident n com = 
-  let ce = constant_entry_of_com com in
-  declare_constant ident (ce,n);
-  if is_verbose() then message ((string_of_id ident) ^ " is defined")
+    { const_entry_body = Cooked (constr_of_com sigma env com);
+      const_entry_type = option_app (constr_of_com1 true sigma env) comtypopt }
 
 let red_constant_entry ce = function
   | None -> ce
@@ -56,12 +46,14 @@ let red_constant_entry ce = function
 	const_entry_type = 
 	  ce.const_entry_type }
 
-let definition_body_red ident n com red_option = 
-  let ce = constant_entry_of_com com in
+let definition_body_red ident n com comtypeopt red_option = 
+  let ce = constant_entry_of_com (com,comtypeopt) in
   let ce' = red_constant_entry ce red_option in
   declare_constant ident (ce',n);
   if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
+let definition_body ident n com typ = definition_body_red ident n com typ None
+
 let syntax_definition ident com =
   let c = raw_constr_of_com Evd.empty (Global.context()) com in 
   Syntax_def.declare_syntactic_definition ident c;
diff --git a/toplevel/command.mli b/toplevel/command.mli
index eaeb289c09..cd4cb930d5 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -10,10 +10,11 @@ open Declare
 (* Declaration functions. The following functions take ASTs, transform them
    into [constr] and then call the corresponding functions of [Declare]. *)
 
-val definition_body : identifier -> strength -> Coqast.t -> unit
+val definition_body : identifier -> strength -> 
+  Coqast.t -> Coqast.t option -> unit
 
-val definition_body_red : identifier -> strength -> Coqast.t 
-  -> Tacred.red_expr option -> unit
+val definition_body_red : identifier -> strength ->
+  Coqast.t -> Coqast.t option -> Tacred.red_expr option -> unit
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 54629fe2d3..e69d537a1a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -724,13 +724,14 @@ let _ =
 let _ =
   add "DEFINITION"
     (function 
-       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c ::optred) ->
-	   let red_option = match optred with 
-	     | [] -> None
-	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] -> 
-		 let env = Global.env() in
-		 let redexp = redexp_of_ast Evd.empty env (r1,r2) in 
-		 Some redexp
+       | (VARG_STRING kind :: VARG_IDENTIFIER id :: VARG_CONSTR c :: rest) ->
+	   let typ_opt,red_option = match rest with
+	     | [] -> None, None
+	     | [VARG_CONSTR t] -> Some t, None
+	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] ->
+		 None, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
+	     | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp(r1,r2))] ->
+		 Some t, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
 	     | _ -> bad_vernac_args "DEFINITION"
 	   in 
 	   let stre,coe,objdef,idcoe = match kind with
@@ -748,7 +749,7 @@ let _ =
              | _       -> anomaly "Unexpected string"
 	   in 
 	   fun () ->
-	     definition_body_red id stre c red_option;
+	     definition_body_red id stre c typ_opt red_option;
              if coe then begin
 	       Class.try_add_new_coercion id stre;
                message ((string_of_id id) ^ " is now a coercion")