Fix de quelques bugs syntaxiques de Ltac

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

4 files changed, 25 insertions, 20 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 2ce4211fc0..24f3a00c9a 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -38,7 +38,9 @@ GEXTEND Gram
   ;
   vrec_clause:
     [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
-          <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
+        <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>>
+      | name=identarg; ":="; body=tactic_expr ->
+        <:ast<(RECCLAUSE $name $body)>> ] ]
   ;
   command:
     [ [ IDENT "Goal"; c = constrarg -> <:ast< (GOAL $c) >>
@@ -103,22 +105,25 @@ GEXTEND Gram
         <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
       | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause  ->
         (match vc with
-            Coqast.Node(_,"RECCLAUSE",nme::tl) ->
-              <:ast<(TACDEF $nme (AST (REC $vc)))>>
-           |_ ->
+         | Coqast.Node(_,"RECCLAUSE",nme::[_;_]) ->
+           <:ast<(TACDEF $nme (AST (REC $vc)))>>
+         | Coqast.Node(_,"RECCLAUSE",nme::[bd]) ->
+           <:ast<(TACDEF $nme (AST $bd))>>
+         | _ ->
              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 "Recursive"; deftok; "Definition"; vc=vrec_clause; "And";
+        vcl=LIST1 vrec_clause SEP "And" ->
         let nvcl=
           List.fold_right
             (fun e b -> match e with
-                Coqast.Node(_,"RECCLAUSE",nme::_) ->
-                  nme::<:ast<(AST (REC $e))>>::b
-               |_ ->
-                 anomalylabstrm "Gram.vernac" [<'sTR
-                   "Not a correct RECCLAUSE">]) (vc::vcl) []
-        in
-          <:ast<(TACDEF ($LIST $nvcl))>>
+             | Coqast.Node(_,"RECCLAUSE",nme::[_;_]) ->
+               nme::<:ast<(AST (REC $e))>>::b
+             | Coqast.Node(_,"RECCLAUSE",nme::[bd]) ->
+               nme::<:ast<(AST $bd)>>::b
+             | _ ->
+               anomalylabstrm "Gram.vernac" [<'sTR
+                 "Not a correct RECCLAUSE">]) (vc::vcl) [] in
+        <:ast<(TACDEF ($LIST $nvcl))>>
 
 (* Hints for Auto and EAuto *)
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index bab0c5afa0..fc455cd212 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -302,18 +302,18 @@ GEXTEND Gram
       | IDENT "Rec"; rc = rec_clause -> <:ast< (REC $rc) >>
       |	IDENT "Rec"; rc = rec_clause; IDENT "In"; body = tactic_expr ->
           <:ast< (REC (RECDECL $rc) $body) >>
-      | IDENT "Rec"; rc = rec_clause; IDENT "And";
-          rcl = LIST1 rec_clause SEP IDENT "And"; IDENT "In";
+      | IDENT "Rec"; rc = rec_clause; "And";
+          rcl = LIST1 rec_clause SEP "And"; IDENT "In";
           body = tactic_expr ->
             <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
-      | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In";
+      | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
           u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
-      |	IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And" ->
+      |	IDENT "Let"; llc = LIST1 let_clause SEP "And" ->
         (match llc with
 	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
           <:ast< (StartProof "LETTOP" $id $c) >>
         | _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
-      |	IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And";
+      |	IDENT "Let"; llc = LIST1 let_clause SEP "And";
         tb = Vernac_.theorem_body; "Qed" ->
         (match llc with
 	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 76ffec9a44..e4edb1fad2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -51,7 +51,7 @@ END
 
 (* Gallina declarations *)
 GEXTEND Gram
-  GLOBAL: gallina gallina_ext thm_tok;
+  GLOBAL: gallina gallina_ext thm_tok theorem_body;
 
   theorem_body_line:
     [ [ n = numarg; ":"; tac = tacarg; "." ->
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 3f1f952497..065ed4350d 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -140,7 +140,7 @@ let init () =
       "Definition"; "Inductive"; "CoInductive"; 
       "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
       "Orelse"; "Proof"; "Qed";
-      "Prop"; "Set"; "Type"
+      "Prop"; "Set"; "Type"; "And"
     ]; (* "let" is not a keyword because #Core#let.cci would not parse *)
   List.iter add_special_token 
     [ ":"; "("; ")"; "["; "]"; "{"; "}"; "_"; ";"; "`"; "``";