Factorisation du '.' final

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

3 files changed, 213 insertions, 218 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 031ec2831..4e4be99d5 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -63,159 +63,159 @@ GEXTEND Gram
   GLOBAL: command;
 
   command:
-    [ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
-      | IDENT "Cd"; "." -> <:ast< (CD) >>
-      | IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
+    [ [ IDENT "Pwd" -> <:ast< (PWD) >>
+      | IDENT "Cd" -> <:ast< (CD) >>
+      | IDENT "Cd"; dir = stringarg -> <:ast< (CD $dir) >>
 
-      | IDENT "Drop"; "." -> <:ast< (DROP) >>
-      | IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>>
-      | "Quit"; "." -> <:ast< (QUIT) >>
+      | IDENT "Drop" -> <:ast< (DROP) >>
+      | IDENT "ProtectedLoop" -> <:ast< (PROTECTEDLOOP)>>
+      | "Quit" -> <:ast< (QUIT) >>
 
-      | IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >>
-      | IDENT "Print"; "." -> <:ast< (PRINT) >>
-      | IDENT "Print"; IDENT "Hint"; "*"; "." 
+      | IDENT "Print"; IDENT "All" -> <:ast< (PrintAll) >>
+      | IDENT "Print" -> <:ast< (PRINT) >>
+      | IDENT "Print"; IDENT "Hint"; "*" 
 	                    -> <:ast< (PrintHint) >>
-      | IDENT "Print"; IDENT "Hint"; s = identarg; "." ->
+      | IDENT "Print"; IDENT "Hint"; s = identarg ->
           <:ast< (PrintHintId $s) >>
-      | IDENT "Print"; IDENT "Hint"; "." ->
+      | IDENT "Print"; IDENT "Hint" ->
           <:ast< (PrintHintGoal) >>
-      | IDENT "Print"; IDENT "HintDb"; s = identarg ; "." ->
+      | IDENT "Print"; IDENT "HintDb"; s = identarg  ->
 	  <:ast< (PrintHintDb $s) >>
-      | IDENT "Print"; IDENT "Section"; s = identarg; "." ->
+      | IDENT "Print"; IDENT "Section"; s = identarg ->
           <:ast< (PrintSec $s) >>
-      | IDENT "Print"; IDENT "States"; "." -> <:ast< (PrintStates) >>
+      | IDENT "Print"; IDENT "States" -> <:ast< (PrintStates) >>
       (* This should be in "syntax" section but is here for factorization *)
-      | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg; "." ->
+      | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg ->
           <:ast< (PrintGrammar $uni $ent) >>
 
-      | IDENT "Locate"; IDENT "File"; f = stringarg; "." ->
+      | IDENT "Locate"; IDENT "File"; f = stringarg ->
 	  <:ast< (LocateFile $f) >>
-      | IDENT "Locate"; IDENT "Library"; id = identarg; "." ->
+      | IDENT "Locate"; IDENT "Library"; id = identarg ->
 	  <:ast< (LocateLibrary $id) >>
-      | IDENT "Locate"; id = qualidarg; "." ->
+      | IDENT "Locate"; id = qualidarg ->
 	  <:ast< (Locate $id) >>
 
       (* Managing load paths *)
       | IDENT "Add"; IDENT "LoadPath"; dir = stringarg; 
-	"as"; alias = qualidarg; "." -> <:ast< (ADDPATH $dir $alias) >>
-      | IDENT "Add"; IDENT "LoadPath"; dir = stringarg; "." ->
+	"as"; alias = qualidarg -> <:ast< (ADDPATH $dir $alias) >>
+      | IDENT "Add"; IDENT "LoadPath"; dir = stringarg ->
 	  <:ast< (ADDPATH $dir) >>
       | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg;
-	"as"; alias=qualidarg; "." -> <:ast< (RECADDPATH $dir $alias) >>
-      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg; "." ->
+	"as"; alias=qualidarg -> <:ast< (RECADDPATH $dir $alias) >>
+      | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = stringarg ->
          <:ast< (RECADDPATH $dir) >>
-      | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg; "." ->
+      | IDENT "Remove"; IDENT "LoadPath"; dir = stringarg ->
 	  <:ast< (DELPATH $dir) >>
-      | IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
+      | IDENT "Print"; IDENT "LoadPath" -> <:ast< (PrintPath) >>
 
        (* For compatibility *)
-      | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg; "." ->
+      | IDENT "AddPath"; dir = stringarg; "as"; alias = qualidarg ->
          <:ast< (ADDPATH $dir $alias) >>
-      | IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
-      | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg; "." ->
+      | IDENT "AddPath"; dir = stringarg -> <:ast< (ADDPATH $dir) >>
+      | IDENT "AddRecPath"; dir = stringarg; "as"; alias=qualidarg ->
          <:ast< (RECADDPATH $dir $alias) >>
-      | IDENT "AddRecPath"; dir = stringarg; "." ->
+      | IDENT "AddRecPath"; dir = stringarg ->
          <:ast< (RECADDPATH $dir) >>
-      | IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
+      | IDENT "DelPath"; dir = stringarg -> <:ast< (DELPATH $dir) >>
 
-      | IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
-      | IDENT "Print"; "Proof"; id = identarg; "." ->
+      | IDENT "Print"; IDENT "Modules" -> <:ast< (PrintModules) >>
+      | IDENT "Print"; "Proof"; id = identarg ->
           <:ast< (PrintOpaqueId $id) >>
 (* Pris en compte dans PrintOption ci-dessous (CADUC) *)
-      | IDENT "Print"; id = qualidarg; "." -> <:ast< (PrintId $id) >>
-      | IDENT "Search"; id = qualidarg; l = in_or_out_modules; "." ->
+      | IDENT "Print"; id = qualidarg -> <:ast< (PrintId $id) >>
+      | IDENT "Search"; id = qualidarg; l = in_or_out_modules ->
 	  <:ast< (SEARCH $id ($LIST $l)) >>
-      | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
-      | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules; "." ->
+      | IDENT "Inspect"; n = numarg -> <:ast< (INSPECT $n) >>
+      | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules ->
 	  <:ast< (SearchPattern $c ($LIST $l)) >>
-      | IDENT "SearchRewrite"; c = constrarg; l = in_or_out_modules; "." ->
+      | IDENT "SearchRewrite"; c = constrarg; l = in_or_out_modules ->
 	  <:ast< (SearchRewrite $c ($LIST $l)) >>
       (* TODO: rapprocher Eval et Check *)
-      | IDENT "Eval"; r = Tactic.red_tactic; "in"; c = constrarg; "." ->
+      | 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 = constrarg; "." ->
+        "in"; c = constrarg ->
           <:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
-      | check = check_tok; c = constrarg; "." -> <:ast< (Check $check $c) >>
-      | check = check_tok; g = numarg; c = constrarg; "." ->
+      | 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"; "." ->
+      | IDENT "Print"; IDENT "ML"; IDENT "Path" ->
           <:ast< (PrintMLPath) >>
-      | IDENT "Print"; IDENT "ML"; IDENT "Modules"; "." ->
+      | IDENT "Print"; IDENT "ML"; IDENT "Modules" ->
           <:ast< (PrintMLModules) >>
-      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg; "." ->
+      | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg ->
           <:ast< (AddMLPath $dir) >>
       | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path";
-        dir = stringarg; "." ->
+        dir = stringarg ->
           <:ast< (RecAddMLPath $dir) >>
-      | IDENT "Print"; IDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
-      | IDENT "Print"; IDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
-      | IDENT "Print"; IDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
-      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg; "." ->
+      | IDENT "Print"; IDENT "Graph" -> <:ast< (PrintGRAPH) >>
+      | IDENT "Print"; IDENT "Classes" -> <:ast< (PrintCLASSES) >>
+      | IDENT "Print"; IDENT "Coercions" -> <:ast< (PrintCOERCIONS) >>
+      | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg ->
           <:ast< (PrintPATH $c $d) >>
 
       | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
-      | IDENT "SearchIsos"; com = constrarg; "." ->
+      | IDENT "SearchIsos"; com = constrarg ->
           <:ast< (Searchisos $com) >>
-      | "Set"; IDENT "Undo"; n = numarg; "." ->
+      | "Set"; IDENT "Undo"; n = numarg ->
           <:ast< (SETUNDO $n) >>
-      | IDENT "Unset"; IDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
-      | "Set"; IDENT "Hyps_limit"; n = numarg; "." ->
+      | IDENT "Unset"; IDENT "Undo" -> <:ast< (UNSETUNDO) >>
+      | "Set"; IDENT "Hyps_limit"; n = numarg ->
           <:ast< (SETHYPSLIMIT $n) >>
-      | IDENT "Unset"; IDENT "Hyps_limit"; "." ->
+      | IDENT "Unset"; IDENT "Hyps_limit" ->
           <:ast< (UNSETHYPSLIMIT) >>
 
       (* Standardized syntax for Implicit Arguments *)
-      | "Set"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+      | "Set"; IDENT "Implicit"; IDENT "Arguments" ->
           <:ast< (IMPLICIT_ARGS_ON) >>
-      | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+      | IDENT "Unset"; IDENT "Implicit"; IDENT "Arguments" ->
           <:ast< (IMPLICIT_ARGS_OFF) >>
-      | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments"; "." ->
+      | IDENT "Test"; IDENT "Implicit"; IDENT "Arguments" ->
           <:ast< (TEST_IMPLICIT_ARGS) >>
 
       (* Pour intervenir sur les tables de paramètres *)
       | "Set"; table = identarg; field = identarg;
-                      value = option_value; "." ->
+                      value = option_value ->
           <:ast< (SetTableField $table $field $value) >>
-      | "Set"; table = identarg; field = identarg; "." ->
+      | "Set"; table = identarg; field = identarg ->
           <:ast< (SetTableField $table $field) >>
-      | IDENT "Unset"; table = identarg; field = identarg; "." ->
+      | IDENT "Unset"; table = identarg; field = identarg ->
           <:ast< (UnsetTableField $table $field) >>
-      | "Set"; table = identarg; value = option_value; "." ->
+      | "Set"; table = identarg; value = option_value ->
           <:ast< (SetTableField $table $value) >>
-      | "Set"; table = identarg; "." ->
+      | "Set"; table = identarg ->
           <:ast< (SetTableField $table) >>
-      | IDENT "Unset"; table = identarg; "." ->
+      | IDENT "Unset"; table = identarg ->
           <:ast< (UnsetTableField $table) >>
       | IDENT "Print"; IDENT "Table";
-		      table = identarg; field = identarg; "." ->
+		      table = identarg; field = identarg ->
           <:ast< (PrintOption $table $field) >>
       (* Le cas suivant inclut aussi le "Print id" standard *)
-      | IDENT "Print"; IDENT "Table"; table = identarg; "." ->
+      | IDENT "Print"; IDENT "Table"; table = identarg ->
           <:ast< (PrintOption $table) >>
-      | IDENT "Add"; table = identarg; field = identarg; id = identarg; "."
+      | IDENT "Add"; table = identarg; field = identarg; id = identarg
         -> <:ast< (AddTableField $table $field $id) >>
-      | IDENT "Add"; table = identarg; field = identarg; id = stringarg; "."
+      | IDENT "Add"; table = identarg; field = identarg; id = stringarg
         -> <:ast< (AddTableField $table $field $id) >>
-      | IDENT "Add"; table = identarg; id = identarg; "."
+      | IDENT "Add"; table = identarg; id = identarg
         -> <:ast< (AddTableField $table $id) >>
-      | IDENT "Add"; table = identarg; id = stringarg; "."
+      | IDENT "Add"; table = identarg; id = stringarg
         -> <:ast< (AddTableField $table $id) >>
-      | IDENT "Test"; table = identarg; field = identarg; id = identarg; "."
+      | IDENT "Test"; table = identarg; field = identarg; id = identarg
         -> <:ast< (MemTableField $table $field $id) >>
-      | IDENT "Test"; table = identarg; field = identarg; id = stringarg; "."
+      | IDENT "Test"; table = identarg; field = identarg; id = stringarg
         -> <:ast< (MemTableField $table $field $id) >>
-      | IDENT "Test"; table = identarg; id = identarg; "."
+      | IDENT "Test"; table = identarg; id = identarg
         -> <:ast< (MemTableField $table $id) >>
-      | IDENT "Test"; table = identarg; id = stringarg; "."
+      | IDENT "Test"; table = identarg; id = stringarg
         -> <:ast< (MemTableField $table $id) >>
-      | IDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
+      | IDENT "Remove"; table = identarg; field = identarg; id = identarg ->
           <:ast< (RemoveTableField $table $field $id) >>
-      | IDENT "Remove"; table = identarg; field = identarg; id = stringarg; "." ->
+      | IDENT "Remove"; table = identarg; field = identarg; id = stringarg ->
           <:ast< (RemoveTableField $table $field $id) >>
-      | IDENT "Remove"; table = identarg; id = identarg; "." ->
+      | IDENT "Remove"; table = identarg; id = identarg ->
           <:ast< (RemoveTableField $table $id) >>
-      | IDENT "Remove"; table = identarg; id = stringarg; "." ->
+      | IDENT "Remove"; table = identarg; id = stringarg ->
           <:ast< (RemoveTableField $table $id) >> ] ]
   ;
   option_value:
@@ -244,20 +244,20 @@ GEXTEND Gram
 	let _ = set_default_action_parser_by_name univ in univ ] ]
   ;
   syntax:
-   [ [ IDENT "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
+   [ [ IDENT "Token"; s = STRING -> <:ast< (TOKEN ($STR $s)) >>
 
      | "Grammar"; univ = univ;
-       tl = LIST1 Prim.grammar_entry SEP "with"; "." ->
+       tl = LIST1 Prim.grammar_entry SEP "with" ->
          <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
 
-     | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
+     | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";" ->
          <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >>
 
      (* Faudrait une version de qualidarg dans Prim pour respecter l'ordre *)
      | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
-       p = qualidarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
+       p = qualidarg -> <:ast< (INFIX (AST $as_) $n $op $p) >>
      | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
-       p = qualidarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
+       p = qualidarg -> <:ast< (DISTFIX (AST $as_) $n $s $p) >>
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index c1b0c9660..d176a05aa 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,76 +34,76 @@ GEXTEND Gram
           <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
-      | IDENT "Goal"; "." -> <:ast< (GOAL) >>
-      | "Proof"; "." -> <:ast< (GOAL) >>
-      |	IDENT "Begin"; "." -> <:ast< (GOAL) >>
-      | IDENT "Abort"; "." -> <:ast< (ABORT) >>
-      | "Qed"; "." -> <:ast< (SaveNamed) >>
-      | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
-      | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
-      |	IDENT "Defined"; id = identarg; "." -> <:ast< (DefinedAnonymous $id) >>
-      | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
+    [ [ IDENT "Goal"; c = constrarg -> <:ast< (GOAL $c) >>
+      | IDENT "Goal" -> <:ast< (GOAL) >>
+      | "Proof" -> <:ast< (GOAL) >>
+      |	IDENT "Begin" -> <:ast< (GOAL) >>
+      | IDENT "Abort" -> <:ast< (ABORT) >>
+      | "Qed" -> <:ast< (SaveNamed) >>
+      | IDENT "Save" -> <:ast< (SaveNamed) >>
+      | IDENT "Defined" -> <:ast< (DefinedNamed) >>
+      |	IDENT "Defined"; id = identarg -> <:ast< (DefinedAnonymous $id) >>
+      | IDENT "Save"; IDENT "Remark"; id = identarg ->
           <:ast< (SaveAnonymousRmk $id) >>
-      | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
+      | IDENT "Save"; IDENT "Theorem"; id = identarg ->
           <:ast< (SaveAnonymousThm $id) >>
-      | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymous $id) >>
-      | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
-      | IDENT "Resume"; "." -> <:ast< (RESUME) >>
-      | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
-      | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
-      | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
-      | IDENT "Restart"; "." -> <:ast< (RESTART) >>
-      | "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) >>
-      | IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
+      | IDENT "Save"; id = identarg -> <:ast< (SaveAnonymous $id) >>
+      | IDENT "Suspend" -> <:ast< (SUSPEND) >>
+      | IDENT "Resume" -> <:ast< (RESUME) >>
+      | IDENT "Resume"; id = identarg -> <:ast< (RESUME $id) >>
+      | IDENT "Abort"; IDENT "All" -> <:ast< (ABORTALL) >>
+      | IDENT "Abort"; id = identarg -> <:ast< (ABORT $id) >>
+      | IDENT "Restart" -> <:ast< (RESTART) >>
+      | "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) >>
+      | IDENT "Show"; IDENT "Implicits"; n = numarg ->
           <:ast< (SHOWIMPL $n) >>
-      | IDENT "Focus"; "." -> <:ast< (FOCUS) >>
-      | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
-      | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
-      | IDENT "Show"; "." -> <:ast< (SHOW) >>
-      | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
-      | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
-      | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
-      | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
-      | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
+      | IDENT "Focus" -> <:ast< (FOCUS) >>
+      | IDENT "Focus"; n = numarg -> <:ast< (FOCUS $n) >>
+      | IDENT "Unfocus" -> <:ast< (UNFOCUS) >>
+      | IDENT "Show" -> <:ast< (SHOW) >>
+      | IDENT "Show"; IDENT "Implicits" -> <:ast< (SHOWIMPL) >>
+      | IDENT "Show"; IDENT "Node" -> <:ast< (ShowNode) >>
+      | IDENT "Show"; IDENT "Script" -> <:ast< (ShowScript) >>
+      | IDENT "Show"; IDENT "Existentials" -> <:ast< (ShowEx) >>
+      | IDENT "Existential"; n = numarg; ":="; c = constrarg ->
           <:ast< (EXISTENTIAL $n $c) >>
       | IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
-        c2 = Constr.constr; "." ->
+        c2 = Constr.constr ->
           <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
       | IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
-        c1 = Constr.constr; "." ->
+        c1 = Constr.constr ->
           <:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
-      | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
+      | IDENT "Explain"; "Proof"; l = numarg_list ->
           <:ast< (ExplainProof ($LIST $l)) >>
-      | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
+      | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list ->
           <:ast< (ExplainProofTree ($LIST $l)) >>
-      | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
-      | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
-      | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
-      | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
-      | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
-      | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
-      | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
-      | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
+      | IDENT "Go"; n = numarg -> <:ast< (Go $n) >>
+      | IDENT "Go"; IDENT "top" -> <:ast< (Go "top") >>
+      | IDENT "Go"; IDENT "prev" -> <:ast< (Go "prev") >>
+      | IDENT "Go"; IDENT "next" -> <:ast< (Go "next") >>
+      | IDENT "Show"; "Proof" -> <:ast< (ShowProof) >>
+      | IDENT "Guarded" -> <:ast< (CheckGuard) >>
+      | IDENT "Show"; IDENT "Tree" -> <:ast< (ShowTree) >>
+      | IDENT "Show"; IDENT "Conjectures" -> <:ast< (ShowProofs) >>
 
 (* Definitions for tactics *)
 
-      | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic;
-        "." -> <:ast<(TACDEF $name (AST $body))>>
+      | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic
+        -> <:ast<(TACDEF $name (AST $body))>>
       | deftok; "Definition"; name=identarg; largs=LIST1 input_fun;
-        ":="; body=Tactic.tactic; "." ->
+        ":="; body=Tactic.tactic ->
         <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
-      | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ; "." ->
+      | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause  ->
         (match vc with
             Coqast.Node(_,"RECCLAUSE",nme::tl) ->
               <:ast<(TACDEF $nme (AST (REC $vc)))>>
            |_ ->
              anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
       |IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause;
-        IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
+        IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And" ->
         let nvcl=
           List.fold_right
             (fun e b -> match e with
@@ -118,36 +118,36 @@ GEXTEND Gram
 (* Hints for Auto and EAuto *)
 
       | IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
-	IDENT "Resolve"; c = constrarg; "." ->
+	IDENT "Resolve"; c = constrarg ->
 	  <:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Immediate"; c = constrarg; "." ->
+	IDENT "Immediate"; c = constrarg ->
 	  <:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Unfold"; c = identarg; "." ->
+	IDENT "Unfold"; c = identarg ->
 	  <:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Constructors"; c = qualidarg;  "." ->
+	IDENT "Constructors"; c = qualidarg ->
 	  <:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
 	  
       | IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
-	IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
+	IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg ->
 	  <:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames)) 
 		   $n $c (TACTIC $tac))>>
 	  
       | IDENT "Hints"; IDENT "Resolve"; l = ne_qualidarg_list; 
-	dbnames = opt_identarg_list; "." ->
+	dbnames = opt_identarg_list ->
           <:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
       | IDENT "Hints"; IDENT "Immediate"; l = ne_qualidarg_list; 
-	dbnames = opt_identarg_list; "." ->
+	dbnames = opt_identarg_list ->
           <:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
       | IDENT "Hints"; IDENT "Unfold"; l = ne_qualidarg_list;
-	dbnames = opt_identarg_list; "." ->
+	dbnames = opt_identarg_list ->
           <:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
 	  
       | IDENT "HintDestruct"; 
@@ -155,14 +155,14 @@ GEXTEND Gram
                 na  = identarg;
                 hyptyp = constrarg;
                 pri = numarg;
-                tac = Prim.astact; "." -> 
+                tac = Prim.astact -> 
           <:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
 
-      | n = numarg; ":"; tac = tacarg; "." ->
+      | n = numarg; ":"; tac = tacarg ->
           <:ast< (SOLVE $n (TACTIC $tac)) >> 
 
 (*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; com = constrarg; "." ->
+      | IDENT "PrintConstr"; com = constrarg ->
           <:ast< (PrintConstr $com)>>
       ] ];
   END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 60b0cb5c1..c0b8e45ab 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,10 +15,12 @@ open Vernac
 GEXTEND Gram
   GLOBAL: vernac;
   vernac:
-    [ [ g = gallina -> g 
-      | g = gallina_ext -> g
-      | c = command -> c 
-      | c = syntax -> c
+    (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
+    (* "." is still in the stream and discard_to_dot works correctly         *)
+    [ [ g = gallina; "." -> g 
+      | g = gallina_ext; "." -> g
+      | c = command; "." -> c 
+      | c = syntax; "." -> c
       | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
   ;
   vernac: LAST
@@ -39,9 +41,9 @@ GEXTEND Gram
   GLOBAL: gallina gallina_ext;
 
   theorem_body_line:
-    [ [ n = numarg; ":"; tac = tacarg; "." ->
+    [ [ n = numarg; ":"; tac = tacarg ->
           <:ast< (VERNACCALL {SOLVE} $n (TACTIC $tac)) >>
-      | tac = tacarg; "." -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
+      | tac = tacarg -> <:ast< (VERNACCALL {SOLVE} 1 (TACTIC $tac)) >>
       ] ]
   ;
   theorem_body_line_list:
@@ -103,40 +105,40 @@ GEXTEND Gram
   ;
   gallina:
     (* Definition, Goal *)
-    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg; "." ->
+    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
           <:ast< (StartProof $thm $id $c) >>
       | thm = thm_tok; id = identarg; ":"; c = constrarg; ":="; "Proof";
-        tb = theorem_body; "Qed"; "." ->
+        tb = theorem_body; "Qed" ->
           <:ast< (TheoremProof $thm $id $c $tb) >>
       | def = def_tok; s = identarg; bl = binders_list;
-	":"; t = Constr.constr; "." ->
+	":"; 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; "." ->
+	":="; 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; "." ->
+	":="; 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; "." ->
+	":"; 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; "." ->
+      | hyp = hyp_tok; bl = ne_params_list ->
           <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
-      | hyp = hyps_tok; bl = ne_params_list; "." ->
+      | hyp = hyps_tok; bl = ne_params_list ->
           <:ast< (VARIABLE $hyp  (BINDERLIST ($LIST $bl))) >>
-      | hyp = param_tok; bl = ne_params_list; "." ->
+      | hyp = param_tok; bl = ne_params_list ->
           <:ast< (PARAMETER $hyp (BINDERLIST ($LIST $bl))) >>
-      | hyp = params_tok; bl = ne_params_list; "." ->
+      | 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; "." ->
+        ":="; c = constrarg ->
           <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
       ] ]
   ;
@@ -270,37 +272,37 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_tok;
-        indl = block_old_style; "." ->
+        indl = block_old_style ->
           <:ast< (OLDMUTUALINDUCTIVE (BINDERLIST ($LIST $bl)) $f
                                      (VERNACARGLIST ($LIST $indl))) >>
       | record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
-	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+	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; "}"; "." ->
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
           <:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
 *)      ] ]
   ;
   gallina:
-    [ [ IDENT "Mutual"; f = finite_tok; indl = block; "." ->
+    [ [ IDENT "Mutual"; f = finite_tok; indl = block ->
           <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
-      | "Fixpoint"; recs = specifrec; "." ->
+      | "Fixpoint"; recs = specifrec ->
           <:ast< (MUTUALRECURSIVE (VERNACARGLIST ($LIST $recs))) >>
-      | "CoFixpoint"; corecs = specifcorec; "." ->
+      | "CoFixpoint"; corecs = specifcorec ->
           <:ast< (MUTUALCORECURSIVE (VERNACARGLIST ($LIST $corecs))) >>
-      | IDENT "Scheme"; schemes = specifscheme; "." ->
+      | IDENT "Scheme"; schemes = specifscheme ->
           <:ast< (INDUCTIONSCHEME (VERNACARGLIST ($LIST $schemes))) >>
       | f = finite_tok; s = sortarg; id = identarg; indpar = indpar; ":=";
-        lc = constructor_list; "." ->
+        lc = constructor_list ->
           <:ast< (ONEINDUCTIVE $f $id $s $indpar $lc) >>
-      | f = finite_tok; indl = block; "." ->
+      | f = finite_tok; indl = block ->
           <:ast< (MUTUALINDUCTIVE $f (VERNACARGLIST ($LIST $indl))) >>
 
       | record_tok; oc = opt_coercion; name = identarg; ps = indpar; ":";
-	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}"; "." ->
+	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; "}"; "." ->
+	s = sortarg; ":="; c = rec_constr; "{"; fs = fields; "}" ->
           <:ast< (RECORD "COERCION" $name $ps $s $c $fs) >>
 *)      ] ];
 
@@ -318,61 +320,54 @@ GEXTEND Gram
   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) >>
+	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_qualidconstarg_list; "." ->
+      | IDENT "Transparent"; l = ne_qualidconstarg_list ->
           <:ast< (TRANSPARENT ($LIST $l)) >>
-      | IDENT "Opaque"; l = ne_qualidconstarg_list; "." -> 
+      | IDENT "Opaque"; l = ne_qualidconstarg_list -> 
 	  <:ast< (OPAQUE ($LIST $l)) >>
 
 (* Coercions *)
-      (* BUG: "Coercion S.T := A." n'est pas reconnu comme une phrase, pq?? *)
-      | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body; "." ->
+      | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body ->
           let s = Ast.coerce_to_var "qid" qid in
           <:ast< (DEFINITION "COERCION" ($VAR $s) $c) >>
-(*
-      | IDENT "Coercion"; qid = qualidarg; ":="; c1 = Constr.constr; ":";
-         c2 = Constr.constr; "." ->
-          let s = Ast.coerce_to_var "qid" qid in
-          <:ast< (DEFINITION "COERCION" ($VAR $s) (CONSTR (CAST $c1 $c2))) >>
-*)
       | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
-	 c = constrarg; "." ->
+	 c = constrarg ->
           <:ast< (DEFINITION "LCOERCION" $s $c) >>
       | IDENT "Coercion"; IDENT "Local"; s = identarg; ":="; 
-	 c1 = Constr.constr; ":"; c2 = Constr.constr; "." ->
+	 c1 = Constr.constr; ":"; c2 = Constr.constr ->
           <:ast< (DEFINITION "LCOERCION" $s (CONSTR (CAST $c1 $c2))) >>
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = qualidarg;
-         ":"; c = qualidarg; ">->"; d = qualidarg; "." ->
+         ":"; c = qualidarg; ">->"; d = qualidarg ->
           <:ast< (COERCION "LOCAL" "IDENTITY" $f $c $d) >>
       | IDENT "Identity"; IDENT "Coercion"; f = qualidarg; ":";
-         c = qualidarg; ">->"; d = qualidarg; "." ->
+         c = qualidarg; ">->"; d = qualidarg ->
           <:ast< (COERCION "" "IDENTITY" $f $c $d) >>
       | IDENT "Coercion"; IDENT "Local"; f = qualidarg; ":"; c = qualidarg;
-        ">->"; d = qualidarg; "." ->
+        ">->"; d = qualidarg ->
           <:ast< (COERCION "LOCAL" "" $f $c $d) >>
       | IDENT "Coercion"; f = qualidarg; ":"; c = qualidarg; ">->";
-         d = qualidarg; "." -> <:ast< (COERCION "" "" $f $c $d) >>
-      | IDENT "Class"; IDENT "Local"; c = qualidarg; "." ->
+         d = qualidarg -> <:ast< (COERCION "" "" $f $c $d) >>
+      | IDENT "Class"; IDENT "Local"; c = qualidarg ->
           <:ast< (CLASS "LOCAL" $c) >>
-      | IDENT "Class"; c = qualidarg; "." -> <:ast< (CLASS "" $c) >>
+      | IDENT "Class"; c = qualidarg -> <:ast< (CLASS "" $c) >>
 
 (* Implicit *)
+      | IDENT "Syntactic"; "Definition"; id = identarg; ":="; com = constrarg
+         -> <:ast< (SyntaxMacro $id $com) >>
       | 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"; "." ->
+         "|"; n = numarg -> <:ast< (SyntaxMacro $id $com $n) >>
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
           <:ast< (IMPLICIT_ARGS_ON) >>
-      | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off"; "." ->
+      | IDENT "Implicit"; IDENT "Arguments"; IDENT "Off" ->
           <:ast< (IMPLICIT_ARGS_OFF) >>
-      | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]"; "." ->
+      | IDENT "Implicits"; id = identarg; "["; l = numarg_list; "]" ->
           <:ast< (IMPLICITS "" $id ($LIST $l)) >>
-      | IDENT "Implicits"; id = identarg; "." ->
+      | IDENT "Implicits"; id = identarg ->
           <:ast< (IMPLICITS "Auto" $id) >> 
   ] ]
   ;
@@ -394,7 +389,7 @@ GEXTEND Gram
   ;
   command:
     [ [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
-	s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
+	s = [ s = STRING -> s | s = IDENT -> s ] ->
           <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
       | "Compile";
 	verbosely =
@@ -405,24 +400,24 @@ GEXTEND Gram
           [ IDENT "Specification" -> "Specification"
           | -> "" ];
 	mname = [ s = STRING -> s | s = IDENT -> s ];
-	fname = OPT [ 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; "." ->
+      | IDENT "Read"; IDENT "Module"; id = identarg ->
           <:ast< (ReadModule $id) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
-        id = identarg; "." -> <:ast< (Require $import $specif $id) >>
+        id = identarg -> <:ast< (Require $import $specif $id) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
-        id = identarg; filename = stringarg; "." ->
+        id = identarg; filename = stringarg ->
           <:ast< (RequireFrom $import $specif $id $filename) >>
-      | IDENT "Write"; IDENT "Module"; id = identarg; "." -> 
+      | IDENT "Write"; IDENT "Module"; id = identarg -> 
 	  <:ast< (WriteModule $id) >>
-      | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg; "." -> 
+      | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg -> 
 	  <:ast< (WriteModule $id $s) >>
       | IDENT "Declare"; IDENT "ML"; IDENT "Module";
-        l = ne_stringarg_list; "." -> <:ast< (DeclareMLModule ($LIST $l)) >>
-      | IDENT "Import"; id = identarg; "." -> <:ast< (ImportModule $id) >>
+        l = ne_stringarg_list -> <:ast< (DeclareMLModule ($LIST $l)) >>
+      | IDENT "Import"; id = identarg -> <:ast< (ImportModule $id) >>
 
   ] 
 ]
@@ -436,27 +431,27 @@ GEXTEND Gram
     [ [ 
 
 (* State management *)
-        IDENT "Write"; IDENT "State"; id = identarg; "." ->
+        IDENT "Write"; IDENT "State"; id = identarg ->
           <:ast< (WriteState $id) >>
-      | IDENT "Write"; IDENT "State"; s = stringarg; "." ->
+      | IDENT "Write"; IDENT "State"; s = stringarg ->
           <:ast< (WriteState $s) >>
-      | IDENT "Restore";  IDENT "State"; id = identarg; "." ->
+      | IDENT "Restore";  IDENT "State"; id = identarg ->
           <:ast< (RestoreState $id) >>
-      | IDENT "Restore";  IDENT "State"; s = stringarg; "." ->
+      | IDENT "Restore";  IDENT "State"; s = stringarg ->
           <:ast< (RestoreState $s) >>
-      | IDENT "Reset"; id = identarg; "." -> <:ast< (ResetName $id) >>
-      | IDENT "Reset"; IDENT "Initial"; "." -> <:ast< (ResetInitial) >>
-      | IDENT "Reset"; IDENT "Section"; id = identarg; "." ->
+      | IDENT "Reset"; id = identarg -> <:ast< (ResetName $id) >>
+      | IDENT "Reset"; IDENT "Initial" -> <:ast< (ResetInitial) >>
+      | IDENT "Reset"; IDENT "Section"; id = identarg ->
           <:ast< (ResetSection $id) >>
       
 (* Extraction *)
-      | IDENT "Extraction"; id = identarg; "." ->
+      | IDENT "Extraction"; id = identarg ->
           <:ast< (PrintExtractId $id) >>
-      | IDENT "Extraction"; "." -> <:ast< (PrintExtract) >>
+      | IDENT "Extraction" -> <:ast< (PrintExtract) >>
 
 (* Tactic Debugger *)
-      |	IDENT "Debug"; IDENT "On"; "." -> <:ast< (DebugOn) >>
-      |	IDENT "Debug"; IDENT "Off"; "." -> <:ast< (DebugOff) >>
+      |	IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >>
+      |	IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >>
 
  ] ];
     END