modules grammaire Coq

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

7 files changed, 1484 insertions, 0 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
new file mode 100644
index 000000000..f06f9228a
--- /dev/null
+++ b/parsing/g_basevernac.ml4
@@ -0,0 +1,185 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA                        ENS-CNRS                *)
+(*              Rocquencourt                        Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                              Jul 10th 1997                               *)
+(*                                                                          *)
+(****************************************************************************)
+(*                             g_basevernac.ml4                             *)
+(****************************************************************************)
+
+(* camlp4o pa_extend.cmo ./q_ast.cma *)
+
+open CoqAst;;
+open Pcoq;;
+
+open Vernac;;
+GEXTEND Gram
+  identarg:
+    [ [ id = LIDENT -> <: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)) ] ]
+  ;
+  ne_numarg_list:
+    [ [ n = numarg; l = ne_numarg_list -> n::l
+      | n = numarg -> [n] ] ]
+  ;
+  numarg_list:
+    [ [ l = ne_numarg_list -> l
+      |  -> [] ] ]
+  ;
+  stringarg:
+    [ [ s = Prim.string -> s ] ]
+  ;
+  comarg:
+    [ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ]
+  ;
+  lcomarg:
+    [ [ c = Command.lcommand -> <:ast< (COMMAND $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)) >> ] ]
+  ;
+  vernac:
+    [ [ LIDENT "Pwd"; "." -> <:ast< (PWD) >>
+      | LIDENT "Cd"; "." -> <:ast< (CD) >>
+      | LIDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
+      | "Quit"; "." -> <:ast< (QUIT) >>
+      | LIDENT "Drop"; "." -> <:ast< (DROP) >>
+      | LIDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >>
+      | LIDENT "Print"; LIDENT "All"; "." -> <:ast< (PrintAll) >>
+      | LIDENT "Print"; "." -> <:ast< (PRINT) >>
+      | LIDENT "Print"; LIDENT "Hint"; "*"; "." 
+	                    -> <:ast< (PrintHint) >>
+      | LIDENT "Print"; LIDENT "Hint"; s = identarg; "." ->
+          <:ast< (PrintHintId $s) >>
+      | LIDENT "Print"; LIDENT "Hint"; "." ->
+          <:ast< (PrintHintGoal) >>
+      | LIDENT "Print"; LIDENT "HintDb"; s = identarg ; "." ->
+	  <:ast< (PrintHintDb $s) >>
+      | LIDENT "Print"; LIDENT "Section"; s = identarg; "." ->
+          <:ast< (PrintSec $s) >>
+      | LIDENT "Print"; LIDENT "States"; "." -> <:ast< (PrintStates) >>
+      | LIDENT "Locate"; LIDENT "File"; f = stringarg; "." ->
+	  <:ast< (LocateFile $f) >>
+      | LIDENT "Locate"; LIDENT "Library"; id = identarg; "." ->
+	  <:ast< (LocateLibrary $id) >>
+      | LIDENT "Locate"; id = identarg; "." ->
+	  <:ast< (Locate $id) >>
+      | LIDENT "Print"; LIDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+      | LIDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
+      | LIDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+      | LIDENT "AddRecPath"; dir = stringarg; "." ->
+          <:ast< (RECADDPATH $dir) >>
+      | LIDENT "Print"; LIDENT "Modules"; "." -> <:ast< (PrintModules) >>
+      | LIDENT "Print"; "Proof"; id = identarg; "." ->
+          <:ast< (PrintOpaqueId $id) >>
+(* Pris en compte dans PrintOption ci-dessous 
+      | LIDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> *)
+      | LIDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
+      | LIDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
+      (* TODO: rapprocher Eval et Check *)
+      | LIDENT "Eval"; r = Tactic.red_tactic; "in"; c = comarg; "." ->
+          <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
+      | LIDENT "Eval"; g = numarg; r = Tactic.red_tactic;
+        "in"; c = comarg; "." ->
+          <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
+      | check = check_tok; c = comarg; "." -> <:ast< (Check $check $c) >>
+      | check = check_tok; g = numarg; c = comarg; "." ->
+          <:ast< (Check $check $c $g) >>
+      | LIDENT "Print"; LIDENT "ML"; LIDENT "Path"; "." ->
+          <:ast< (PrintMLPath) >>
+      | LIDENT "Print"; LIDENT "ML"; LIDENT "Modules"; "." ->
+          <:ast< (PrintMLModules) >>
+      | LIDENT "Add"; LIDENT "ML"; LIDENT "Path"; dir = stringarg; "." ->
+          <:ast< (AddMLPath $dir) >>
+      | LIDENT "Add"; LIDENT "Rec"; LIDENT "ML"; LIDENT "Path";
+        dir = stringarg; "." ->
+          <:ast< (RecAddMLPath $dir) >>
+      | LIDENT "Print"; LIDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
+      | LIDENT "Print"; LIDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
+      | LIDENT "Print"; LIDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
+      | LIDENT "Print"; LIDENT "Path"; c = identarg; d = identarg; "." ->
+          <:ast< (PrintPATH $c $d) >>
+
+(*      | LIDENT "Time"; "." -> <:ast< (Time) >>
+      | LIDENT "Untime"; "." -> <:ast< (Untime) >> *)
+
+      | LIDENT "Time"; v = vernac -> <:ast< (Time $v)>>
+      | LIDENT "SearchIsos"; com = comarg; "." ->
+          <:ast< (Searchisos $com) >>
+      | "Set"; LIDENT "Undo"; n = numarg; "." ->
+          <:ast< (SETUNDO $n) >>
+      | LIDENT "Unset"; LIDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
+      | "Set"; LIDENT "Hyps_limit"; n = numarg; "." ->
+          <:ast< (SETHYPSLIMIT $n) >>
+      | LIDENT "Unset"; LIDENT "Hyps_limit"; "." ->
+          <:ast< (UNSETHYPSLIMIT) >>
+
+      (* Pour intervenir sur les tables de paramètres *)
+      | "Set"; table = identarg; field = identarg;
+                      value = option_value; "." ->
+          <:ast< (SetTableField $table $field $value) >>
+      | "Set"; table = identarg; field = identarg; "." ->
+          <:ast< (SetTableField $table $field) >>
+      | LIDENT "Unset"; table = identarg; field = identarg; "." ->
+          <:ast< (UnsetTableField $table $field) >>
+      | "Set"; table = identarg; value = option_value; "." ->
+          <:ast< (SetTableField $table $value) >>
+      | "Set"; table = identarg; "." ->
+          <:ast< (SetTableField $table) >>
+      | LIDENT "Unset"; table = identarg; "." ->
+          <:ast< (UnsetTableField $table) >>
+      | LIDENT "Print"; table = identarg; field = identarg; "." ->
+          <:ast< (PrintOption $table $field) >>
+      (* Le cas suivant inclut aussi le "Print id" standard *)
+      | LIDENT "Print"; table = identarg; "." ->
+          <:ast< (PrintOption $table) >>
+      | LIDENT "Add"; table = identarg; field = identarg; id = identarg; "."
+        -> <:ast< (AddTableField $table $field $id) >>
+      | LIDENT "Add"; table = identarg; id = identarg; "."
+        -> <:ast< (AddTableField $table $id) >>
+      | LIDENT "Test"; table = identarg; field = identarg; id = identarg; "."
+        -> <:ast< (MemTableField $table $field $id) >>
+      | LIDENT "Test"; table = identarg; id = identarg; "."
+        -> <:ast< (MemTableField $table $id) >>
+      | LIDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
+          <:ast< (RemoveTableField $table $field $id) >>
+      | LIDENT "Remove"; table = identarg; id = identarg; "." ->
+          <:ast< (RemoveTableField $table $id) >> ] ]
+  ;
+  option_value:
+    [ [ id = identarg    -> id
+      | n  = numarg      -> n
+      | s  = stringarg   -> s ] ]
+  ;
+  check_tok:
+    [ [ LIDENT "Check" -> <:ast< "CHECK" >>
+      | "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
+  ;
+END;
+
+(* $Id$ *)
diff --git a/parsing/g_command.ml4 b/parsing/g_command.ml4
new file mode 100644
index 000000000..9066b77b5
--- /dev/null
+++ b/parsing/g_command.ml4
@@ -0,0 +1,200 @@
+
+(* $Id$ *)
+
+open Pcoq
+
+open Command
+
+GEXTEND Gram
+  ident:
+    [ [ id = LIDENT -> <:ast< ($VAR $id) >> ] ]
+  ;
+  raw_command:
+    [ [ c = Prim.ast -> c ] ]
+  ;
+  command:
+    [ [ c = command8 -> c ] ]
+  ;
+  lcommand:
+    [ [ c = command10 -> c ] ]
+  ;
+  ne_command_list:
+    [ [ c1 = command; cl = ne_command_list -> c1::cl
+      | c1 = command -> [c1] ] ]
+  ;
+  command0:
+    [ [ "?" -> <:ast< (XTRA "ISEVAR") >>
+      | "?"; n = Prim.number -> <:ast< (META $n) >>
+      | "["; id1 = LIDENT; ":"; c = command; c2 = abstraction_tail ->
+          <:ast< (LAMBDA $c [$id1]$c2) >>
+      | "["; id1 = LIDENT; ","; idl = ne_ident_comma_list;
+        ":"; c = command; c2 = abstraction_tail ->
+          <:ast< (LAMBDALIST $c [$id1]($SLAM $idl $c2)) >>
+      | "["; id1 = LIDENT; ","; idl = ne_ident_comma_list;
+             c = abstraction_tail ->
+          <:ast< (LAMBDALIST (XTRA "ISEVAR") [$id1]($SLAM $idl $c)) >>
+      | "["; id1 = LIDENT; c = abstraction_tail ->
+          <:ast< (LAMBDA (XTRA "ISEVAR") [$id1]$c) >>
+      | "["; id1 = LIDENT; "="; c = command; "]"; c2 = command ->
+          <:ast< (ABST #Core#let.cci $c [$id1]$c2) >> 
+      | "<<"; id1 = LIDENT; ">>"; c = command -> <:ast< [$id1]$c >>
+      | "("; lc1 = lcommand; ":"; c = command; body = product_tail ->
+          let id = Ast.coerce_to_var "lc1" lc1 in
+            <:ast< (PROD $c [$id]$body) >>
+      | "("; lc1 = lcommand; ","; lc2 = lcommand; ":"; c = command; 
+        body = product_tail ->
+          let id1 = Ast.coerce_to_var "lc1" lc1 in
+          let id2 = Ast.coerce_to_var "lc2" lc2 in
+            <:ast< (PRODLIST $c [$id1][$id2]$body) >>
+      | "("; lc1 = lcommand; ","; lc2 = lcommand; ",";
+        idl = ne_ident_comma_list; ":"; c = command; body = product_tail ->
+          let id1 = Ast.coerce_to_var "lc1" lc1 in
+          let id2 = Ast.coerce_to_var "lc2" lc2 in
+            <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
+      | "("; lc1 = lcommand; ")" -> lc1
+      | "("; lc1 = lcommand; ")"; "@"; "["; cl = ne_command_list; "]" ->
+          <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
+      | "Prop" -> <:ast< (PROP {Null}) >>
+      | "Set" -> <:ast< (PROP {Pos}) >>
+      | "Type" -> <:ast< (TYPE) >>
+      | LIDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
+          <:ast< (FIX $id ($LIST $fbinders)) >>
+      | LIDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
+          <:ast< (COFIX $id ($LIST $fbinders)) >>
+      | v = ident -> v ] ]
+  ;
+  command1:
+    [ [ "<"; ":"; LIDENT "ast"; ":"; "<"; c = raw_command; ">>" -> c
+      | "<"; l1 = lcommand; ">"; LIDENT "Match"; c = command; "with";
+        cl = ne_command_list; "end" ->
+          <:ast< (XTRA "REC" $l1 $c ($LIST $cl)) >>
+      | "<"; l1 = lcommand; ">"; LIDENT "Match"; c = command; "with"; "end"
+        ->
+          <:ast< (XTRA "REC" $l1 $c) >>
+      | "<"; l1 = lcommand; ">"; LIDENT "Case"; c = command; "of";
+        cl = ne_command_list; "end" ->
+          <:ast< (MUTCASE $l1 $c ($LIST $cl)) >>
+      | "<"; l1 = lcommand; ">"; LIDENT "Case"; c = command; "of"; "end" ->
+          <:ast< (MUTCASE $l1 $c) >>
+      | LIDENT "Case"; c = command; "of"; cl = ne_command_list; "end" ->
+          <:ast< (XTRA "MLCASE" "NOREC" $c ($LIST $cl)) >>
+      | LIDENT "Case"; c = command; "of"; "end" ->
+          <:ast< (XTRA "MLCASE" "NOREC" $c) >>
+      | LIDENT "Match"; c = command; "with"; cl = ne_command_list; "end" ->
+          <:ast< (XTRA "MLCASE" "REC" $c ($LIST $cl)) >>
+      | LIDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+        c = command; "in"; c1 = command ->
+          <:ast< (XTRA "MLCASE" "NOREC" $c (LAMBDALIST (XTRA "ISEVAR")
+                   ($SLAM $b $c1))) >>
+      | LIDENT "let"; id1 = LIDENT ; "="; c = command; "in";
+        c1 = command -> <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>
+      | LIDENT "if"; c1 = command; LIDENT "then"; c2 = command;
+        LIDENT "else"; c3 = command ->
+        <:ast< ( XTRA "MLCASE" "NOREC" $c1 $c2 $c3) >>
+(* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *)
+      | "<"; l1 = lcommand; ">";
+        LIDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
+        c = command; "in"; c1 = command ->
+         <:ast< (MUTCASE $l1 $c (LAMBDALIST (XTRA "ISEVAR") ($SLAM $b $c1))) >>
+      | "<"; l1 = lcommand; ">";
+        LIDENT "if"; c1 = command; LIDENT "then";
+        c2 = command; LIDENT "else"; c3 = command ->
+          <:ast< (MUTCASE $l1 $c1 $c2 $c3) >>
+      | c = command0 -> c ] ]
+  ;
+  command2:
+    [ [ c = command1 -> c ] ]
+  ;
+  command3:
+    [ [ c1 = command2 -> c1 ] ]
+  ;
+  lassoc_command4:
+    [ [ c1 = command3 -> c1 ] ]
+  ;
+  command5:
+    [ [ c1 = lassoc_command4 -> c1
+      | c1 = lassoc_command4; "::"; c2 = command5 ->
+          <:ast< (CAST $c1 $c2) >> ] ]
+  ;
+  command6:
+    [ [ c1 = command5 -> c1 ] ]
+  ;
+  command7:
+    [ RIGHTA [ c1 = command6 -> c1 ] ]
+  ;
+  command8:
+    [ [ c1 = command7 -> c1
+      | c1 = command7; "->"; c2 = command8 ->
+          <:ast< (PROD $c1 [<>]$c2) >> ] ]
+  ;
+  command9:
+    [ [ c1 = command8 -> c1 ] ]
+  ;
+  command10:
+    [ [ "!"; f = LIDENT; args = ne_command9_list ->
+          <:ast< (APPLIST (XTRA "!" ($VAR $f)) ($LIST $args)) >>
+      | f = command9; args = ne_command91_list ->
+          <:ast< (APPLIST $f ($LIST $args)) >>
+      | f = command9 -> f ] ]
+  ;
+  ne_ident_comma_list:
+    [ [ id = ident; ","; idl = ne_ident_comma_list -> id::idl
+      | id = ident -> [id] ] ]
+  ;
+  binder:
+    [ [ idl = ne_ident_comma_list; ":"; c = command ->
+          <:ast< (BINDER $c ($LIST $idl)) >> ] ]
+  ;
+  ne_binder_list:
+    [ [ id = binder; ";"; idl = ne_binder_list -> id::idl
+      | id = binder -> [id] ] ]
+  ;
+  command91:
+    [ [ n = Prim.number; "!"; c1 = command9 ->
+          <:ast< (XTRA "!" $n $c1) >>
+      | c1 = command9 -> c1 ] ]
+  ;
+  ne_command91_list:
+    [ [ c1 = command91; cl = ne_command91_list -> c1::cl
+      | c1 = command91 -> [c1] ] ]
+  ;
+  ne_command9_list:
+    [ [ c1 = command9; cl = ne_command9_list -> c1::cl
+      | c1 = command9 -> [c1] ] ]
+  ;
+  fixbinder:
+    [ [ id = ident; "/"; recarg = Prim.number; ":"; type_ = command;
+        ":="; def = command -> <:ast< (NUMFDECL $id $recarg $type_ $def) >>
+      | id = ident; "["; idl = ne_binder_list; "]"; ":"; type_ = command;
+        ":="; def = command ->
+          <:ast< (FDECL $id (BINDERS ($LIST $idl)) $type_ $def) >> ] ]
+  ;
+  fixbinders:
+    [ [ fb = fixbinder; "with"; fbs = fixbinders -> fb::fbs
+      | fb = fixbinder -> [fb] ] ]
+  ;
+  cofixbinder:
+    [ [ id = ident; ":"; type_ = command; ":="; def = command ->
+          <:ast< (CFDECL $id $type_ $def) >> ] ]
+  ;
+  cofixbinders:
+    [ [ fb = cofixbinder; "with"; fbs = cofixbinders -> fb::fbs
+      | fb = cofixbinder -> [fb] ] ]
+  ;
+  abstraction_tail:
+    [ [ ";"; idl = ne_ident_comma_list;
+        ":"; c = command; c2 = abstraction_tail ->
+          <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >>
+      | ";"; idl = ne_ident_comma_list; c2 = abstraction_tail ->
+          <:ast< (LAMBDALIST (XTRA "ISEVAR") ($SLAM $idl $c2)) >>
+      | "]"; c = command -> c ] ]
+  ;
+  product_tail:
+    [ [ ";"; idl = ne_ident_comma_list;
+        ":"; c = command; c2 = product_tail ->
+          <:ast< (PRODLIST $c ($SLAM $idl $c2)) >>
+      | ";"; idl = ne_ident_comma_list; c2 = product_tail ->
+          <:ast< (PRODLIST (XTRA "ISEVAR") ($SLAM $idl $c2)) >>
+      | ")"; c = command -> c ] ]
+  ;
+END
diff --git a/parsing/g_multiple_case.ml4 b/parsing/g_multiple_case.ml4
new file mode 100644
index 000000000..4c20e3a27
--- /dev/null
+++ b/parsing/g_multiple_case.ml4
@@ -0,0 +1,74 @@
+
+(* $Id$ *)
+
+open Pcoq
+
+open Command
+
+GEXTEND Gram
+  pattern_list:
+    [ [  -> ([],[])
+      | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2,[p :: pl]) ] ]
+  ;
+  lsimple_pattern:
+    [ [ c = simple_pattern2 -> c ] ]
+  ;
+  simple_pattern:
+    [ [ id = ident -> ([Ast.nvar_of_ast id], id)
+      | "("; p = lsimple_pattern; ")" -> p ] ]
+  ;
+  simple_pattern_list:
+    [ [  -> ([],[])
+      | (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list ->
+	   (id1@id2,[p :: pl]) ] ]
+  ;
+  (* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
+     since params are not given in patterns *)
+  simple_pattern2:
+    [ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list ->
+          (id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>)
+      | (id1,p) = simple_pattern; "as"; id = ident ->
+          ([Ast.nvar_of_ast id::id1], <:ast< (XTRA"AS" $id $p) >>)
+      | (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern ->
+          (id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ]
+  ;
+  pattern:
+    [ [ p = simple_pattern -> p ] ]
+  ;
+  ne_pattern_list:
+    [ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list ->
+	(id1@id2, [c1 :: cl])
+      | (id1,c1) = pattern -> (id1,[c1]) ] ]
+  ;
+  equation:
+    [ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command ->
+          let br =
+	    List.fold_right (fun s ast -> CoqAst.Slam loc (Some s) ast)
+	      ids
+	      <:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in
+	  let lid = List.map (fun s -> CoqAst.Id loc s) ids in
+	  <:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ]
+  ;
+  ne_eqn_list:
+    [ [ e = equation; "|"; leqn = ne_eqn_list -> [e :: leqn]
+      | e = equation -> [e] ] ]
+  ;
+
+  command1:
+    [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+        OPT "|"; eqs = ne_eqn_list; "end" ->
+          <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))
+                    ($LIST $eqs)) >>
+      | "Cases"; lc = ne_command_list; "of"; 
+	OPT "|"; eqs = ne_eqn_list; "end" ->
+          <:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
+                    (XTRA"TOMATCH"($LIST $lc)) ($LIST $eqs)) >>
+      | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+        "end" ->
+          <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))) >>
+      | "Cases"; lc = ne_command_list; "of"; "end" -> 
+          <:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
+                    (XTRA"TOMATCH"($LIST $lc))) >> ] ]
+  ;
+  END
+
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
new file mode 100644
index 000000000..9ccc40ea3
--- /dev/null
+++ b/parsing/g_prim.ml4
@@ -0,0 +1,73 @@
+
+(* $Id$ *)
+
+open Coqast
+open Pcoq
+
+open Prim
+
+GEXTEND Gram
+  GLOBAL: var ident number string path ast astpat astact entry_type;
+
+  var:
+    [ [ s = LIDENT -> Nvar(loc,s) ] ]
+  ;
+  ident:
+    [ [ s = LIDENT -> Id(loc,s) ] ]
+  ;
+  number:
+    [ [ i = INT -> Num(loc, int_of_string i) ] ]
+  ;
+  string:
+    [ [ s = STRING -> Str(loc,s) ] ]
+  ;
+  path:
+    [ [ (l,pk) = qualid -> Path(loc,l,pk) ] ]
+  ;
+  qualid:
+    [ [ "#"; l = LIST1 LIDENT SEP "#"; "."; pk = LIDENT -> (l, pk) ] ]
+  ;
+
+  (* ast *)
+  ast:
+    [ [ id = LIDENT -> Nvar(loc,id)
+      | s = INT -> Num(loc, int_of_string s)
+      | s = STRING -> Str(loc,s)
+      | p = path -> p
+      | "{"; s = LIDENT; "}" -> Id(loc,s)
+      | "("; nname = LIDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
+      | "["; ido = idoption; "]"; b = ast -> Slam(loc,ido,b)
+      | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
+  ;
+  idoption:
+    [ [ "<>" -> None
+      | id = LIDENT -> Some id ] ]
+  ;
+
+  (* meta-syntax entries *)
+  astpat:
+    [ [ a = ast -> Node loc "ASTPAT" [a] ] ]
+  ; 
+  astact:
+    [ [ a = action -> Node loc "ASTACT" [a] ] ]
+  ;
+  astlist:
+    [ [ l = LIST0 ast -> Node loc "ASTLIST" l ] ]
+  ;
+  action:
+    [ [ LIDENT "let"; p = astlist; et = entry_type; "="; e1 = action; "in";
+        e = action -> Node(loc,"$CASE",[e1; et; Node(loc,"CASE",[p;e])])
+      | LIDENT "case"; a = action; et = entry_type; "of";
+        cl = LIST1 case SEP "|"; LIDENT "esac" ->
+          Node(loc,"$CASE",a::et::cl)
+      | "["; al = astlist; "]" -> al ] ]
+  ;
+  case:
+    [[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
+  ;
+  entry_type:
+    [[ ":"; LIDENT "List" -> Id(loc,"LIST")
+     | ":"; LIDENT "Ast" -> Id(loc,"AST")
+     | -> Id(loc,"AST") ]]
+  ;
+END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
new file mode 100644
index 000000000..a4e847c29
--- /dev/null
+++ b/parsing/g_tactic.ml4
@@ -0,0 +1,323 @@
+
+(* $Id$ *)
+
+open Pp
+open Ast
+open Pcoq
+
+open Tactic
+
+(* Please leave several GEXTEND for modular compilation under PowerPC *)
+
+(* Auxiliary grammar rules *)
+
+GEXTEND Gram
+  identarg:
+    [ [ id = LIDENT -> <:ast< ($VAR $id) >> ] ]
+  ;
+  numarg:
+    [ [ n = Prim.number -> n
+      | "-"; n = Prim.number -> CoqAst.Num (Ast.loc n, ( - Ast.num_of_ast n))
+      ] ]
+  ;
+  comarg:
+    [ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ]
+  ;
+  lcomarg:
+    [ [ c = Command.lcommand -> <:ast< (COMMAND $c) >> ] ]
+  ;
+  ne_identarg_list:
+    [ [ l = LIST1 identarg -> l ] ]
+  ;
+  ne_num_list:
+    [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
+  ;
+  pattern_occ:
+    [ [ nl = ne_num_list; c = comarg -> <:ast< (PATTERN $c ($LIST $nl)) >>
+      | c = comarg -> <:ast< (PATTERN $c) >> ] ]
+  ;
+  ne_pattern_list:
+    [ [ l = LIST1 pattern_occ -> l ] ]
+  ;
+  pattern_occ_hyp:
+    [ [ nl = ne_num_list; LIDENT "Goal" -> <:ast<(CCLPATTERN ($LIST $nl))>>
+      | nl = ne_num_list; id = identarg -> <:ast<(HYPPATTERN $id ($LIST $nl))>>
+      | LIDENT "Goal" -> <:ast< (CCLPATTERN) >>
+      | id = identarg -> <:ast< (HYPPATTERN $id) >> ] ]
+  ;
+  ne_pattern_hyp_list:
+    [ [ l = LIST1 pattern_occ_hyp -> l ] ]
+  ;
+  one_intropattern:
+    [ [ p= ne_intropattern ->  <:ast< (INTROPATTERN $p)>> ]]
+  ;
+  ne_intropattern:
+    [ [   tc = LIST1 simple_intropattern -> 
+           <:ast< (LISTPATTERN ($LIST $tc))>> ] ]
+  ;
+  simple_intropattern:
+    [ [ "["; tc = LIST1 intropattern  SEP "|" ; "]" -> 
+         <:ast< (DISJPATTERN ($LIST $tc)) >>
+      | "("; tc = LIST1 intropattern SEP "," ; ")" -> 
+         <:ast< (CONJPATTERN ($LIST $tc)) >>
+      | id = identarg                   -> 
+         <:ast< (IDENTIFIER $id) >> ] ]
+  ;
+  intropattern:
+    [ [   tc = LIST1 simple_intropattern -> 
+              <:ast< (LISTPATTERN ($LIST $tc))>>
+         | -> <:ast< (LISTPATTERN) >> ]]
+  ;
+  simple_binding:
+    [ [ id = identarg; ":="; c = comarg -> <:ast< (BINDING $id $c) >>
+      | n = numarg; ":="; c = comarg -> <:ast< (BINDING $n $c) >> ] ]
+  ;
+  simple_binding_list:
+    [ [ b = simple_binding; l = simple_binding_list -> b :: l | -> [] ] ]
+  ;
+  com_binding_list:
+    [ [ c = comarg; bl = com_binding_list -> <:ast< (BINDING $c) >> :: bl
+      | -> [] ] ]
+  ;
+  binding_list:
+    [ [ c1 = comarg; ":="; c2 = comarg; bl = simple_binding_list ->
+          let id = match c1 with 
+            | CoqAst.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
+            | _ -> assert false
+          in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>>
+      | n = numarg; ":="; c = comarg; bl = simple_binding_list ->
+          <:ast<(BINDINGS (BINDING $n $c) ($LIST $bl))>>
+      | c1 = comarg; bl = com_binding_list ->
+          <:ast<(BINDINGS (BINDING $c1) ($LIST $bl))>>
+      | -> <:ast<(BINDINGS)>> ] ]
+  ;
+  with_binding_list:
+    [ [ "with"; l = binding_list -> l | -> <:ast<(BINDINGS)>> ] ]
+  ;
+  comarg_binding_list:
+    [ [ c = comarg; l = with_binding_list -> [c; l] ] ]
+  ;
+  numarg_binding_list:
+    [ [ n = numarg; l = with_binding_list -> [n; l] ] ]
+  ;
+  comarg_list:
+    [ [ c = comarg; l = comarg_list -> c :: l | -> [] ] ]
+  ;
+  unfold_occ:
+    [ [ nl = ne_num_list; c = identarg -> <:ast< (UNFOLD $c ($LIST $nl)) >>
+      | c = identarg -> <:ast< (UNFOLD $c) >> ] ]
+  ;
+  ne_unfold_occ_list:
+    [ [ p = unfold_occ; l = ne_unfold_occ_list -> p :: l
+      | p = unfold_occ -> [p] ] ]
+  ;
+  red_flag:
+    [ [ LIDENT "Beta" -> <:ast< (Beta) >>
+      | LIDENT "Delta" -> <:ast< (Delta) >>
+      | LIDENT "Iota" -> <:ast< (Iota) >>
+      | "["; idl = ne_identarg_list; "]" -> <:ast< (Unf ($LIST idl)) >>
+      | "-"; "["; idl = ne_identarg_list; "]" ->
+          <:ast< (UnfBut ($LIST idl)) >> ] ]
+  ;
+  red_tactic:
+    [ [ LIDENT "Red" -> <:ast< (Red) >>
+      | LIDENT "Hnf" -> <:ast< (Hnf) >>
+      | LIDENT "Simpl" -> <:ast< (Simpl) >>
+      | LIDENT "Cbv"; s = LIST1 red_flag -> <:ast< (Cbv ($LIST s)) >>
+      | LIDENT "Lazy"; s = LIST1 red_flag -> <:ast< (Lazy ($LIST s)) >>
+      | LIDENT "Compute" -> <:ast< (Cbv (Beta) (Delta) (Iota)) >>
+      | LIDENT "Unfold"; ul = ne_unfold_occ_list ->
+          <:ast< (Unfold ($LIST ul)) >>
+      | LIDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
+      | LIDENT "Change"; c = comarg -> <:ast< (Change $c) >>
+      | LIDENT "Pattern"; pl = ne_pattern_list ->
+          <:ast< (Pattern ($LIST $pl)) >> ] ]
+  ;
+  clausearg:
+    [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
+      | -> <:ast< (CLAUSE) >> ] ]
+  ;
+  autoarg_depth:
+  [ [ n = numarg -> <:ast< $n>>
+     | -> CoqAst.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_adding:
+  [ [ LIDENT "Adding" ; "["; l = ne_identarg_list; "]" -> 
+        <:ast< (CLAUSE ($LIST $l))>>
+      | -> <:ast< (CLAUSE) >> ] ]
+  ;
+  autoarg_destructing:
+  [ [ LIDENT "Destructing" -> CoqAst.Str(loc,"Destructing")
+      | -> CoqAst.Str(loc,"NoAutoArg") ] ]
+  ;
+  autoarg_usingTDB:
+  [ [ "Using"; "TDB"  ->  CoqAst.Str(loc,"UsingTDB")
+      | -> CoqAst.Str(loc,"NoAutoArg")  ] ]
+  ;
+  fixdecl:
+    [ [ id = identarg; n = numarg; ":"; c = comarg; fd = fixdecl ->
+          <:ast< (FIXEXP $id $n $c) >> :: fd
+      | -> [] ] ]
+  ;
+  cofixdecl:
+    [ [ id = identarg; ":"; c = comarg; fd = cofixdecl ->
+          <:ast< (COFIXEXP $id $c) >> :: fd
+      | -> [] ] ]
+  ;
+ END
+
+(* Tactics grammar rules *)
+
+GEXTEND Gram
+  tactic_com_list:
+    [ [ y = tactic_com; ";"; l = LIST1 tactic_com_tail SEP ";" ->
+          <:ast< (TACTICLIST $y ($LIST $l)) >>
+      | y = tactic_com -> <:ast< (TACTICLIST $y) >> ] ]
+  ;
+  tactic_com_tail:
+    [ [ t1 = tactic_com -> t1
+      | "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
+          <:ast< (TACLIST ($LIST $l)) >> ] ]
+  ;
+  tactic_com:
+    [ [ st = simple_tactic; "Orelse"; tc = tactic_com ->
+          <:ast< (ORELSE $st $tc) >>
+      | st = simple_tactic -> st ] ]
+  ;
+  simple_tactic:
+    [ [ LIDENT "Fix"; n = numarg -> <:ast< (Fix $n) >>
+      | LIDENT "Fix"; id = identarg; n = numarg -> <:ast< (Fix $id $n) >>
+      | LIDENT "Fix"; id = identarg; n = numarg; "with"; fd = fixdecl ->
+          <:ast< (Fix $id $n ($LIST $fd)) >>
+      | LIDENT "Cofix" -> <:ast< (Cofix) >>
+      | LIDENT "Cofix"; id = identarg -> <:ast< (Cofix $id) >>
+      | LIDENT "Cofix"; id = identarg; "with"; fd = cofixdecl ->
+          <:ast< (Cofix $id ($LIST $fd)) >>
+      | LIDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
+      | LIDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
+      | LIDENT "Double"; LIDENT "Induction"; i = numarg; j = numarg ->
+          <:ast< (DoubleInd $i $j) >>
+      | LIDENT "Trivial" -> <:ast<(Trivial)>>
+      | LIDENT "Trivial"; "with"; lid = ne_identarg_list -> 
+	  <:ast<(Trivial ($LIST $lid))>>
+      | LIDENT "Trivial"; "with"; "*" ->  <:ast<(Trivial "*")>>
+      | LIDENT "Auto"; n = numarg -> <:ast< (Auto $n) >>
+      | LIDENT "Auto" -> <:ast< (Auto) >>
+      | LIDENT "Auto"; n = numarg; "with";
+	  lid = ne_identarg_list -> <:ast< (Auto $n ($LIST $lid)) >>
+      | LIDENT "Auto"; "with";
+	  lid = ne_identarg_list -> <:ast< (Auto ($LIST $lid)) >>
+      | LIDENT "Auto"; n = numarg; "with"; "*" ->
+	  <:ast< (Auto $n "*") >>
+      | LIDENT "Auto"; "with"; "*" -> <:ast< (Auto "*") >>
+     
+      | LIDENT "AutoTDB"; n = numarg -> <:ast< (AutoTDB $n) >>
+      | LIDENT "AutoTDB" -> <:ast< (AutoTDB) >>
+      | LIDENT "DHyp";  id=identarg  -> <:ast< (DHyp  $id)>>
+      | LIDENT "CDHyp"; id=identarg -> <:ast<  (CDHyp $id)>>
+      | LIDENT "DConcl"  -> <:ast< (DConcl)>>
+      | LIDENT "SuperAuto"; 
+                       a0 = autoarg_depth;
+                       a1 = autoarg_adding; 
+                       a2 = autoarg_destructing; 
+                       a3 = autoarg_usingTDB -> 
+                   <:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
+      | LIDENT "Auto"; n = numarg; LIDENT "Decomp" -> <:ast< (DAuto $n) >>
+      | LIDENT "Auto"; LIDENT "Decomp" -> <:ast< (DAuto) >>
+      | LIDENT "Auto"; n = numarg; LIDENT "Decomp"; p = numarg-> <:ast< (DAuto $n $p) >>
+      ]];
+    END
+
+GEXTEND Gram
+ simple_tactic:
+  [ [  LIDENT "Intros" -> <:ast< (Intros) >>
+      | LIDENT "Intros"; LIDENT "until"; id = identarg 
+                                              -> <:ast< (IntrosUntil $id) >>
+      | LIDENT "Intros"; LIDENT "until"; n = numarg -> <:ast<(IntrosUntil $n)>>
+      | LIDENT "Intros"; pl = one_intropattern -> <:ast< (Intros $pl) >>
+      | LIDENT "Intro"; id = identarg; 
+	  LIDENT "after"; id2 = identarg -> <:ast< (IntroMove $id $id2) >>
+      | LIDENT "Intro";
+	  LIDENT "after"; id2 = identarg -> <:ast< (IntroMove $id2) >>
+      | LIDENT "Intro"; id = identarg -> <:ast< (Intro $id) >>
+      | LIDENT "Intro" -> <:ast< (Intro) >>
+      | LIDENT "Apply"; cl = comarg_binding_list ->
+          <:ast< (Apply ($LIST $cl)) >>
+      | LIDENT "Elim"; cl = comarg_binding_list; "using";
+        el = comarg_binding_list ->
+          <:ast< (Elim ($LIST $cl) ($LIST $el)) >>
+      | LIDENT "Elim"; cl = comarg_binding_list ->
+          <:ast< (Elim ($LIST $cl)) >>
+      | LIDENT "Assumption" -> <:ast< (Assumption) >>
+      | LIDENT "Contradiction" -> <:ast< (Contradiction) >>
+      | LIDENT "Exact"; c = comarg -> <:ast< (Exact $c) >>
+      | LIDENT "OldElim"; c = comarg -> <:ast< (OldElim $c) >>
+      | LIDENT "ElimType"; c = comarg -> <:ast< (ElimType $c) >>
+      | LIDENT "Case"; cl = comarg_binding_list ->
+          <:ast< (Case ($LIST $cl)) >>
+      | LIDENT "CaseType"; c = comarg -> <:ast< (CaseType $c) >>
+      | LIDENT "Destruct"; s = identarg -> <:ast< (Destruct $s) >>
+      | LIDENT "Destruct"; n = numarg -> <:ast< (Destruct $n) >>
+      | LIDENT "Decompose"; LIDENT "Record" ; c = comarg -> 
+             <:ast< (DecomposeAnd $c) >>
+      | LIDENT "Decompose"; LIDENT "Sum"; c = comarg -> 
+             <:ast< (DecomposeOr $c) >>
+      | LIDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = comarg ->
+          <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
+      |	LIDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
+          <:ast<(FIRST ($LIST $l))>>
+      |	LIDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
+          <:ast<(TCLSOLVE ($LIST $l))>>
+      | LIDENT "Cut"; c = comarg -> <:ast< (Cut $c) >>
+      | LIDENT "Specialize"; n = numarg; lcb = comarg_binding_list ->
+          <:ast< (Specialize $n ($LIST $lcb))>>
+      | LIDENT "Specialize"; lcb = comarg_binding_list ->
+          <:ast< (Specialize ($LIST $lcb)) >>
+      | LIDENT "Generalize"; lc = comarg_list ->
+          <:ast< (Generalize ($LIST $lc)) >>
+      | LIDENT "Generalize"; LIDENT "Dependent"; c = comarg ->
+          <:ast< (GeneralizeDep $c) >>
+      | LIDENT "Let"; s = identarg; ":="; c = comarg; "in";
+	  l = ne_pattern_hyp_list -> 
+	    <:ast< (LetTac $s $c (LETPATTERNS ($LIST $l))) >>
+      | LIDENT "LApply"; c = comarg -> <:ast< (CutAndApply $c) >>
+      | LIDENT "Clear"; l = ne_identarg_list -> 
+                <:ast< (Clear (CLAUSE ($LIST $l))) >>
+      | LIDENT "Move"; id1 = identarg; LIDENT "after"; id2 = identarg -> 
+                <:ast< (MoveDep $id1 $id2) >>
+      | LIDENT "Do"; n = numarg; tc = tactic_com -> <:ast< (DO $n $tc) >>
+      | LIDENT "Try"; tc = tactic_com -> <:ast< (TRY $tc) >>
+      | LIDENT "Info"; tc = tactic_com -> <:ast< (INFO $tc) >>
+      | LIDENT "Repeat"; tc = tactic_com -> <:ast< (REPEAT $tc) >>
+      | LIDENT "Abstract"; tc = tactic_com -> <:ast< (ABSTRACT (TACTIC $tc)) >>
+      | LIDENT "Abstract"; tc = tactic_com; "using";  s=identarg 
+                                   -> <:ast< (ABSTRACT $s (TACTIC $tc)) >>
+      | LIDENT "Left"; bl = with_binding_list -> <:ast< (Left $bl) >>
+      | LIDENT "Right"; bl = with_binding_list -> <:ast< (Right $bl) >>
+      | LIDENT "Split"; bl = with_binding_list -> <:ast< (Split $bl) >>
+      | LIDENT "Exists"; bl = binding_list -> <:ast< (Split $bl) >>
+      | LIDENT "Constructor"; nbl = numarg_binding_list ->
+          <:ast<(Constructor ($LIST $nbl)) >>
+      | LIDENT "Constructor" -> <:ast<(Constructor) >>
+      | LIDENT "Reflexivity" -> <:ast< (Reflexivity) >>
+      | LIDENT "Symmetry" -> <:ast< (Symmetry) >>
+      | LIDENT "Transitivity"; c = comarg -> <:ast< (Transitivity $c) >>
+      | LIDENT "Absurd"; c = comarg -> <:ast< (Absurd $c) >>
+      | LIDENT "Idtac" -> <:ast< (Idtac) >>
+      | LIDENT "Fail" -> <:ast< (Fail) >>
+      | "("; tcl = tactic_com_list; ")" -> tcl
+      | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >> ]
+
+    | [ id = identarg; l = comarg_list ->
+          match (isMeta (nvar_of_ast id), l) with
+            | (true, []) -> id
+            | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
+            | _ -> user_err_loc
+                  (loc, "G_tactic.meta_tactic",
+                   [< 'sTR"Cannot apply arguments to a meta-tactic." >])
+      ] ]
+  ;
+  tactic:
+    [ [ tac = tactic_com_list -> tac ] ]
+  ;
+END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
new file mode 100644
index 000000000..740498fad
--- /dev/null
+++ b/parsing/g_vernac.ml4
@@ -0,0 +1,526 @@
+
+(* $Id$ *)
+
+open Pcoq
+
+open Tactic
+
+GEXTEND Gram
+  simple_tactic:
+    [ [ LIDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ] ]
+  ;
+END
+
+open Vernac
+
+GEXTEND Gram
+  vernac: LAST
+    [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ]
+  ;
+END
+
+GEXTEND Gram
+  tacarg:
+    [ [ tcl = Tactic.tactic_com_list -> tcl ] ]
+  ;
+  theorem_body_line:
+    [ [ n = numarg; ":"; tac = tacarg; "." ->
+          <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >>
+      | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
+      ] ]
+  ;
+  theorem_body_line_list:
+    [ [ t = theorem_body_line -> [t]
+      | t = theorem_body_line; l = theorem_body_line_list -> t :: l ] ]
+  ;
+  theorem_body:
+    [ [ l = theorem_body_line_list ->
+          <:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
+  ;
+  destruct_location :
+  [ [ LIDENT "Conclusion"  -> <:ast< (CONCL)>>
+    | LIDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
+    | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
+  ;
+  ne_comarg_list:
+  [ [ l = LIST1 comarg -> l ] ]
+  ;
+
+  opt_identarg_list:
+  [ [ -> []
+    | ":"; l = LIST1 identarg -> l ] ]
+  ;
+
+  finite_tok:
+    [ [ "Inductive" -> <:ast< "Inductive" >>
+      | "CoInductive" -> <:ast< "CoInductive" >> ] ]
+  ;
+  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) >> ] ]
+  ;
+  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) >> ] ]
+  ;
+  onerec:
+    [ [ id = identarg; "["; idl = ne_binder_semi_list; "]"; ":"; c = comarg;
+        ":="; def = comarg ->
+          <:ast< (VERNACARGLIST $id (BINDERLIST ($LIST $idl)) $c $def) >> ] ]
+  ;
+  specifrec:
+    [ [ rec_ = onerec; "with"; recl = specifrec -> rec_ :: recl
+      | rec_ = onerec -> [rec_] ] ]
+  ;
+  onecorec:
+    [ [ id = identarg; ":"; c = comarg; ":="; def = comarg ->
+          <: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:
+    [ [ LIDENT "Record" -> <:ast< "Record" >>
+      | LIDENT "Structure" -> <:ast< "Structure" >> ] ]
+  ;
+  field:
+    [ [ id = identarg; ":"; c = Command.command ->
+          <:ast< (VERNACARGLIST "" $id (COMMAND $c)) >>
+      | id = identarg; ":>"; c = Command.command ->
+          <:ast< (VERNACARGLIST "COERCION" $id (COMMAND $c)) >> ] ]
+  ;
+  nefields:
+    [ [ idc = field; ";"; fs = nefields -> idc :: fs
+      | idc = field -> [idc] ] ]
+  ;
+  fields:
+    [ [ fs = nefields -> <:ast< (VERNACARGLIST ($LIST $fs)) >>
+      |  -> <:ast< (VERNACARGLIST) >> ] ]
+  ;
+  onescheme:
+    [ [ id = identarg; ":="; dep = dep; c = comarg; LIDENT "Sort";
+        s = sortdef ->
+          <:ast< (VERNACARGLIST $id $dep $c (COMMAND $s)) >> ] ]
+  ;
+  specifscheme:
+    [ [ rec_ = onescheme; "with"; recl = specifscheme -> rec_ :: recl
+      | rec_ = onescheme -> [rec_] ] ]
+  ;
+  dep:
+    [ [ LIDENT "Induction"; LIDENT "for" -> <:ast< "DEP" >>
+      | LIDENT "Minimality"; LIDENT "for" -> <:ast< "NODEP" >> ] ]
+  ;
+  ne_binder_semi_list:
+    [ [ id = binder; ";"; idl = ne_binder_semi_list -> id :: idl
+      | id = binder -> [id] ] ]
+  ;
+  indpar:
+    [ [ "["; bl = ne_binder_semi_list; "]" ->
+          <:ast< (BINDERLIST ($LIST $bl)) >>
+      |  -> <:ast< (BINDERLIST) >> ] ]
+  ;
+  sortdef:
+    [ [ "Set" -> <:ast< (PROP {Pos}) >>
+      | "Prop" -> <:ast< (PROP {Null}) >>
+      | "Type" -> <:ast< (TYPE) >> ] ]
+  ;
+  thm_tok:
+    [ [ "Theorem" -> <:ast< "THEOREM" >>
+      | LIDENT "Lemma" -> <:ast< "LEMMA" >>
+      | LIDENT "Fact" -> <:ast< "FACT" >>
+      | LIDENT "Remark" -> <:ast< "REMARK" >> ] ]
+  ;
+
+  def_tok:
+    [ [ "Definition" -> <:ast< "DEFINITION" >>
+      | LIDENT "Local" -> <:ast< "LOCAL" >> 
+      | "@"; "Definition"  -> <:ast< "OBJECT" >>
+      | "@"; LIDENT "Local"  -> <:ast< "LOBJECT" >>
+      | "@"; LIDENT "Coercion"  -> <:ast< "OBJCOERCION" >>
+      | "@"; LIDENT "Local"; LIDENT "Coercion"  -> <:ast< "LOBJCOERCION" >>
+      | LIDENT "SubClass"  -> <:ast< "SUBCLASS" >>
+      | LIDENT "Local"; LIDENT "SubClass"  -> <:ast< "LSUBCLASS" >> ] ]  
+  ;
+  import_tok:
+    [ [ LIDENT "Import" -> <:ast< "IMPORT" >>
+      | LIDENT "Export" -> <:ast< "EXPORT" >>
+      |  -> <:ast< "IMPORT" >> ] ]
+  ;
+  specif_tok:
+    [ [ LIDENT "Implementation" -> <:ast< "IMPLEMENTATION" >>
+      | LIDENT "Specification" -> <:ast< "SPECIFICATION" >>
+      |  -> <:ast< "UNSPECIFIED" >> ] ]
+  ;
+  hyp_tok:
+    [ [ "Hypothesis" -> <:ast< "HYPOTHESIS" >>
+      | "Variable" -> <:ast< "VARIABLE" >> ] ]
+  ;
+  hyps_tok:
+    [ [ LIDENT "Hypotheses" -> <:ast< "HYPOTHESES" >>
+      | LIDENT "Variables" -> <:ast< "VARIABLES" >> ] ]
+  ;
+  param_tok:
+    [ [ "Axiom" -> <:ast< "AXIOM" >>
+      | "Parameter" -> <:ast< "PARAMETER" >> ] ]
+  ;
+  params_tok:
+    [ [ LIDENT "Parameters" -> <:ast< "PARAMETERS" >> ] ]
+  ;
+  binder:
+    [ [ idl = ne_identarg_comma_list; ":"; c = Command.command ->
+          <:ast< (BINDER $c ($LIST $idl)) >> ] ]
+  ;
+  idcom:
+    [ [ id = LIDENT; ":"; c = Command.command ->
+          <:ast< (BINDER $c ($VAR $id)) >> ] ]
+  ;
+  ne_lidcom:
+    [ [ idc = idcom; "|"; l = ne_lidcom -> idc :: l
+      | idc = idcom -> [idc] ] ]
+  ;
+  lidcom:
+    [ [ l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >>
+      | "|"; l = ne_lidcom -> <:ast< (BINDERLIST ($LIST $l)) >>
+      |  -> <:ast< (BINDERLIST) >> ] ]
+  ;
+  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 = Command.command; "." ->
+          <:ast< (StartProof $def $s (COMMAND $c1)) >>
+      | def = def_tok; s = identarg; ":="; c1 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s (COMMAND $c1)) >>
+      | def = def_tok; s = identarg; ":="; c1 = Command.command; ":";
+        c2 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s (COMMAND (CAST $c1 $c2))) >>
+      | def = def_tok; s = identarg; ":"; c1 = Command.command; ":=";
+        c2 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s (COMMAND (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; ":="; 
+      LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s (COMMAND $c1) (TACTIC_ARG (REDEXP $r))) >>
+      | def = def_tok; s = identarg; ":="; 
+      LIDENT "Eval"; r = Tactic.red_tactic; "in"; c1 = Command.command; ":";
+        c2 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s 
+                 (COMMAND (CAST $c1 $c2)) (TACTIC_ARG (REDEXP $r))) >>
+      | def = def_tok; s = identarg; ":"; c1 = Command.command; ":=";
+        LIDENT "Eval"; r = Tactic.red_tactic; "in"; 
+	c2 = Command.command; "." ->
+          <:ast< (DEFINITION $def $s (COMMAND (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 = LIDENT; ":"; 
+	c = Command.command; t = definition_tail;  "." -> 
+	  <:ast< (DEFINITION $def $s (COMMAND (LAMBDA $c [$id1]$t))) >>
+
+      | def = def_tok; s = identarg; "["; id1 = LIDENT; ",";
+	idl = Command.ne_ident_comma_list; ":"; c = Command.command; 
+	t = definition_tail; "." -> 
+	  <:ast< (DEFINITION $def $s (COMMAND 
+			(LAMBDALIST $c [$id1]($SLAM $idl $t)))) >>
+
+
+      | hyp = hyp_tok; bl = ne_binder_semi_list; "." ->
+          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
+      | hyp = hyps_tok; bl = ne_binder_semi_list; "." ->
+          <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
+      | hyp = param_tok; bl = ne_binder_semi_list; "." ->
+          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
+      | hyp = params_tok; bl = ne_binder_semi_list; "." ->
+          <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
+      | LIDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
+        ":="; c = comarg; "." ->
+          <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
+      | f = finite_tok; "Set"; id = identarg; indpar = indpar; ":=";
+        lidcom = lidcom; "." ->
+          <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Pos})) $indpar
+                   $lidcom) >>
+      | f = finite_tok; "Type"; id = identarg; indpar = indpar; ":=";
+        lidcom = lidcom; "." ->
+          <:ast< (ONEINDUCTIVE $f $id (COMMAND (TYPE)) $indpar $lidcom) >>
+      | f = finite_tok; "Prop"; id = identarg; indpar = indpar; ":=";
+        lidcom = lidcom; "." ->
+          <:ast< (ONEINDUCTIVE $f $id (COMMAND (PROP {Null})) $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 (COMMAND $s) $c $fs) >>
+      | record_tok; ">"; name = identarg; ps = indpar; ":"; s = sortdef; ":=";
+        c = rec_constr; "{"; fs = fields; "}"; "." ->
+          <:ast< (RECORD "COERCION" $name $ps (COMMAND $s) $c $fs) >>
+
+      | LIDENT "Mutual"; "["; bl = ne_binder_semi_list; "]" ; f = finite_tok;
+        indl = block_old_style; "." ->
+          <:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
+                                     (VERNACARGLIST ($LIST $indl))) >>
+      | LIDENT "Mutual"; f = finite_tok; indl = block; "." ->
+          <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
+      | "Fixpoint"; recs = specifrec; "." ->
+          <:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >>
+      | "CoFixpoint"; corecs = specifcorec; "." ->
+          <:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >>
+      | LIDENT "Scheme"; schemes = specifscheme; "." ->
+          <:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >>
+      ] ];
+
+      
+      definition_tail:
+    	[ [ ";"; idl = Command.ne_ident_comma_list;
+            ":"; c = Command.command; c2 = definition_tail ->
+              <:ast< (LAMBDALIST $c ($SLAM $idl $c2)) >>
+	| "]"; ":"; ty = Command.command; ":=" ; c = Command.command -> 
+	    <:ast< (CAST $c $ty) >>
+ 	| "]"; ":="; c = Command.command -> c 
+	] ];
+
+  END
+
+(* State management *)
+GEXTEND Gram
+  vernac:
+    [ [ 
+        LIDENT "Save"; LIDENT "State"; id = identarg; "." ->
+          <:ast< (SaveState $id "") >>
+      | LIDENT "Save"; LIDENT "State"; id = identarg; s = stringarg; "." ->
+          <:ast< (SaveState $id $s) >>
+      | LIDENT "Write"; LIDENT "States"; id = identarg; "." ->
+          <:ast< (WriteStates $id) >>
+      | LIDENT "Write"; LIDENT "States"; id = stringarg; "." ->
+          <:ast< (WriteStates $id) >>
+      | LIDENT "Restore";  LIDENT "State"; id = identarg; "." ->
+          <:ast< (RestoreState $id) >>
+      | LIDENT "Remove";  LIDENT "State"; id = identarg; "." ->
+          <:ast< (RemoveState $id) >>
+      | LIDENT "Reset"; LIDENT "after"; id = identarg; "." ->
+          <:ast< (ResetAfter $id) >>
+      | LIDENT "Reset"; LIDENT "Initial"; "." -> <:ast< (ResetInitial) >>
+      | LIDENT "Reset"; LIDENT "Section"; id = identarg; "." ->
+          <:ast< (ResetSection $id) >>
+      | LIDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
+
+(* Modules and Sections *)   
+
+      | LIDENT "Read"; LIDENT "Module"; id = identarg; "." ->
+          <:ast< (ReadModule $id) >>
+      | LIDENT "Require"; import = import_tok; specif = specif_tok;
+        id = identarg; "." -> <:ast< (Require $import $specif $id) >>
+      | LIDENT "Require"; import = import_tok; specif = specif_tok;
+        id = identarg; filename = stringarg; "." ->
+          <:ast< (RequireFrom $import $specif $id $filename) >>
+      | LIDENT "Section"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+      | LIDENT "Chapter"; id = identarg; "." -> <:ast< (BeginSection $id) >>
+      | LIDENT "Module"; id = identarg; "." -> <:ast< (BeginModule $id) >>
+      | LIDENT "Begin"; LIDENT "Silent"; "." -> <:ast< (BeginSilent) >>
+      | LIDENT "End"; LIDENT "Silent"; "." -> <:ast< (EndSilent) >>
+      | LIDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >>
+      | LIDENT "Declare"; LIDENT "ML"; LIDENT "Module";
+        l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
+      | LIDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
+	  (* Transparent and Opaque *)
+      | LIDENT "Transparent"; l = ne_identarg_list; "." ->
+          <:ast< (TRANSPARENT ($LIST $l)) >>
+      | LIDENT "Opaque"; l = ne_identarg_list; "." -> 
+	  <:ast< (OPAQUE ($LIST $l)) >>
+      
+	  (* Extraction *)
+      | LIDENT "Extraction"; id = identarg; "." ->
+          <:ast< (PrintExtractId $id) >>
+      | LIDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
+
+(* Grammar extensions, Coercions, Implicits *)
+	  
+     | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; "." ->
+         <:ast< (DEFINITION "COERCION" $s (COMMAND $c1)) >>
+     | LIDENT "Coercion"; s = identarg; ":="; c1 = Command.command; ":";
+        c2 = Command.command; "." ->
+          <:ast< (DEFINITION "COERCION" $s (COMMAND (CAST $c1 $c2))) >>
+     | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":="; 
+	c1 = Command.command; "." ->
+          <:ast< (DEFINITION "LCOERCION" $s (COMMAND $c1)) >>
+     | LIDENT "Coercion"; LIDENT "Local"; s = identarg; ":="; 
+	c1 = Command.command; ":"; c2 = Command.command; "." ->
+          <:ast< (DEFINITION "LCOERCION" $s (COMMAND (CAST $c1 $c2))) >>
+	  
+	  
+     | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
+        "." -> <:ast< (SyntaxMacro $id $com) >>
+     | LIDENT "Syntactic"; "Definition"; id = identarg; ":="; com = comarg;
+        "|"; n = numarg; "." -> <:ast< (SyntaxMacro $id $com $n) >>
+     | LIDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
+         <:ast< (PrintGrammar $uni $ent) >>
+     | LIDENT "Identity"; LIDENT "Coercion"; LIDENT "Local"; f = identarg;
+        ":"; c = identarg; ">->"; d = identarg; "." ->
+          <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
+     | LIDENT "Identity"; LIDENT "Coercion"; f = identarg; ":";
+        c = identarg; ">->"; d = identarg; "." ->
+          <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
+     | LIDENT "Coercion"; LIDENT "Local"; f = identarg; ":"; c = identarg;
+        ">->"; d = identarg; "." ->
+          <:ast< (COERCION "LOCAL" "" $f $c $d) >>
+     | LIDENT "Coercion"; f = identarg; ":"; c = identarg; ">->";
+        d = identarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
+     | LIDENT "Class"; LIDENT "Local"; c = identarg; "." ->
+         <:ast< (CLASS "LOCAL" $c) >>
+     | LIDENT "Class"; c = identarg; "." -> <:ast< (CLASS "" $c) >>
+     | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "On"; "." ->
+         <:ast< (IMPLICIT_ARGS_ON) >>
+     | LIDENT "Implicit"; LIDENT "Arguments"; LIDENT "Off"; "." ->
+         <:ast< (IMPLICIT_ARGS_OFF) >>
+     | LIDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
+         <:ast< (IMPLICITS "" $id ($LIST $l)) >>
+     | LIDENT "Implicits"; id = identarg; "." ->
+         <:ast< (IMPLICITS "Auto" $id) >> 
+ ] ];
+    END
+
+(* Proof commands *)
+GEXTEND Gram
+  vernac:
+    [ [ LIDENT "Goal"; c = comarg; "." -> <:ast< (GOAL $c) >>
+      | LIDENT "Goal"; "." -> <:ast< (GOAL) >>
+      | "Proof"; "." -> <:ast< (GOAL) >>
+      | LIDENT "Abort"; "." -> <:ast< (ABORT) >>
+      | "Qed"; "." -> <:ast< (SaveNamed) >>
+      | LIDENT "Save"; "." -> <:ast< (SaveNamed) >>
+      | LIDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
+      | LIDENT "Save"; LIDENT "Remark"; id = identarg; "." ->
+          <:ast< (SaveAnonymousRmk $id) >>
+      | LIDENT "Save"; LIDENT "Theorem"; id = identarg; "." ->
+          <:ast< (SaveAnonymousThm $id) >>
+      | LIDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
+      | LIDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
+      | LIDENT "Resume"; "." -> <:ast< (RESUME) >>
+      | LIDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
+      | LIDENT "Abort"; LIDENT "All"; "." -> <:ast< (ABORTALL) >>
+      | LIDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
+      | LIDENT "Restart"; "." -> <:ast< (RESTART) >>
+      | "Proof"; c = comarg; "." -> <:ast< (PROOF $c) >>
+      | LIDENT "Undo"; "." -> <:ast< (UNDO 1) >>
+      | LIDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
+      | LIDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
+      | LIDENT "Show"; LIDENT "Implicits"; n = numarg; "." ->
+          <:ast< (SHOWIMPL $n) >>
+      | LIDENT "Focus"; "." -> <:ast< (FOCUS) >>
+      | LIDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
+      | LIDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
+      | LIDENT "Show"; "." -> <:ast< (SHOW) >>
+      | LIDENT "Show"; LIDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
+      | LIDENT "Show"; LIDENT "Node"; "." -> <:ast< (ShowNode) >>
+      | LIDENT "Show"; LIDENT "Script"; "." -> <:ast< (ShowScript) >>
+      | LIDENT "Show"; LIDENT "Existentials"; "." -> <:ast< (ShowEx) >>
+      | LIDENT "Existential"; n = numarg; ":="; c = Command.command; "." ->
+          <:ast< (EXISTENTIAL $n (COMMAND $c)) >>
+      | LIDENT "Existential"; n = numarg; ":="; c1 = Command.command; ":";
+        c2 = Command.command; "." ->
+          <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >>
+      | LIDENT "Existential"; n = numarg; ":"; c2 = Command.command; ":=";
+        c1 = Command.command; "." ->
+          <:ast< (EXISTENTIAL $n (COMMAND (CAST $c1 $c2))) >>
+      | LIDENT "Explain"; "Proof"; l = numarg_list; "." ->
+          <:ast< (ExplainProof ($LIST $l)) >>
+      | LIDENT "Explain"; "Proof"; LIDENT "Tree"; l = numarg_list; "." ->
+          <:ast< (ExplainProofTree ($LIST $l)) >>
+      | LIDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
+      | LIDENT "Go"; LIDENT "top"; "." -> <:ast< (Go "top") >>
+      | LIDENT "Go"; LIDENT "prev"; "." -> <:ast< (Go "prev") >>
+      | LIDENT "Go"; LIDENT "next"; "." -> <:ast< (Go "next") >>
+      | LIDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
+      | LIDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
+      | LIDENT "Show"; LIDENT "Tree"; "." -> <:ast< (ShowTree) >>
+      | LIDENT "Show"; LIDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
+
+(* Tactic Definition *)
+
+      | LIDENT "Tactic"; "Definition"; id = identarg; "[";
+        ids = ne_identarg_list; "]"; ":="; tac = Prim.astact; "." ->
+          <:ast< (TacticDefinition $id (AST $tac) ($LIST $ids)) >>
+      | LIDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact;
+        "." -> <:ast< (TacticDefinition $id (AST $tac)) >>
+
+(* Hints for Auto and EAuto *)
+
+      | LIDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
+	LIDENT "Resolve"; c = comarg; "." ->
+	  <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
+	  
+      | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	LIDENT "Immediate"; c = comarg; "." ->
+	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	LIDENT "Unfold"; c = identarg; "." ->
+	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	LIDENT "Constructors"; c = identarg;  "." ->
+	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
+	  
+      | LIDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
+	LIDENT "Extern"; n = numarg; c = comarg ; tac = tacarg; "." ->
+	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
+		   $n $c (TACTIC $tac))>>
+	  
+      | LIDENT "Hints"; LIDENT "Resolve"; l = ne_identarg_list; 
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | LIDENT "Hints"; LIDENT "Immediate"; l = ne_identarg_list; 
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | LIDENT "Hints"; LIDENT "Unfold"; l = ne_identarg_list;
+	dbnames = opt_identarg_list; "." ->
+          <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
+	  
+      | LIDENT "HintDestruct"; 
+                dloc = destruct_location;
+                na  = identarg;
+                hyptyp = comarg;
+                pri = numarg;
+                tac = Prim.astact; "." -> 
+          <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
+
+      | n = numarg; ":"; tac = tacarg; "." ->
+          <:ast< (SOLVE $n (TACTIC $tac)) >> 
+
+(*This entry is not commented, only for debug*)
+      | LIDENT "PrintConstr"; com = comarg; "." ->
+          <:ast< (PrintConstr $com)>>
+      ] ];
+  END
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
new file mode 100644
index 000000000..a33288189
--- /dev/null
+++ b/parsing/q_coqast.ml4
@@ -0,0 +1,103 @@
+
+let dummy_loc = (0,0)
+
+let is_meta s = String.length s > 0 && s.[0] == '$'
+
+let not_impl name x =
+  let desc =
+    if Obj.is_block (Obj.repr x) then
+      "tag = " ^ string_of_int (Obj.tag (Obj.repr x))
+    else 
+      "int_val = " ^ string_of_int (Obj.magic x)
+  in
+  failwith ("<Q_coqast." ^ name ^ ", not impl: " ^ desc)
+
+let purge_str s =
+  if String.length s == 0 || s.[0] <> '$' then s
+  else String.sub s 1 (String.length s - 1)
+
+let anti loc x =
+  let e =
+    let loc = (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >>
+  in
+  <:expr< $anti:e$ >>
+
+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
+  | Coqast.Node _ "$VAR" [Coqast.Nvar loc x] ->
+      <:expr< Coqast.Nvar loc $anti loc x$ >>
+  | Coqast.Node _ "$ID" [Coqast.Nvar loc x] ->
+      <:expr< Coqast.Id loc $anti loc x$ >>
+  | Coqast.Node _ "$STR" [Coqast.Nvar loc x] ->
+      <: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$ >>
+  | Coqast.Node loc nn al ->
+      let e = expr_list_of_ast_list al in
+      <:expr< Coqast.Node loc $str:nn$ $e$ >>
+  | Coqast.Nvar loc id -> <:expr< Coqast.Nvar loc $str:id$ >>
+  | Coqast.Slam loc None a ->
+      <:expr< Coqast.Slam loc None $expr_of_ast a$ >>
+  | Coqast.Slam loc (Some s) a ->
+      let se = if is_meta s then anti loc s else <:expr< $str:s$ >> in
+      <:expr< Coqast.Slam loc (Some $se$) $expr_of_ast a$ >>
+  | Coqast.Num loc i -> <:expr< Coqast.Num loc $int:string_of_int i$ >>
+  | Coqast.Id loc id -> <:expr< Coqast.Id loc $str:id$ >>
+  | Coqast.Str loc str -> <:expr< Coqast.Str loc $str:str$ >>
+  | Coqast.Path loc sl s ->
+      let e = expr_list_of_var_list sl in
+      <:expr< Coqast.Path loc $e$ $str:s$ >> 
+  | Coqast.Dynamic _ _ ->
+      failwith "Q_Coqast: dynamic: not implemented"
+
+and expr_list_of_ast_list al =
+  List.fold_right
+    (fun a e2 -> match a with
+       | (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$) >>
+       | _ ->
+           let e1 = expr_of_ast a in
+           let loc = (fst(MLast.loc_of_expr e1), snd(MLast.loc_of_expr e2)) in
+	   <:expr< [$e1$ :: $e2$] >> )
+    al (let loc = dummy_loc in <:expr< [] >>)
+
+and expr_list_of_var_list sl =
+  let loc = dummy_loc in
+  List.fold_right
+    (fun s e2 ->
+       let e1 = if is_meta s then anti loc s else <:expr< $str:s$ >> in
+       let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+       <:expr< [$e1$ :: $e2$] >>)
+    sl <:expr< [] >>
+  
+let rec patt_of_expr e =
+  let loc = MLast.loc_of_expr e in
+  match e with
+    | <:expr< $e1$.$e2$ >> -> <:patt< $patt_of_expr e1$.$patt_of_expr e2$ >>
+    | <:expr< $e1$ $e2$ >> -> <:patt< $patt_of_expr e1$ $patt_of_expr e2$ >>
+    | <:expr< loc >> -> <:patt< _ >>
+    | <:expr< $lid:s$ >> -> <:patt< $lid:s$ >>
+    | <:expr< $uid:s$ >> -> <:patt< $uid:s$ >>
+    | <:expr< $str:s$ >> -> <:patt< $str:s$ >>
+    | <:expr< $anti:e$ >> -> <:patt< $anti:patt_of_expr e$ >>
+    | _ -> not_impl "patt_of_expr" e
+
+let f e =
+  let ee s =
+    expr_of_ast (Pcoq.Gram.Entry.parse e
+                     (Pcoq.Gram.parsable (Stream.of_string s)))
+  in
+  let ep s = patt_of_expr (ee s) in
+  Quotation.ExAst (ee, ep)
+
+let _ = 
+  Quotation.add "command" (f Pcoq.Command.command_eoi);
+  Quotation.add "tactic" (f Pcoq.Tactic.tactic_eoi);
+  Quotation.add "vernac" (f Pcoq.Vernac.vernac_eoi);
+  Quotation.add "ast" (f Pcoq.Prim.ast_eoi);
+  Quotation.default := "command"
+