diff options
| author | delahaye | 2001-06-11 11:57:16 +0000 |
|---|---|---|
| committer | delahaye | 2001-06-11 11:57:16 +0000 |
| commit | dd0cf23cd41386cf028aa212487c35f54f149e70 (patch) | |
| tree | aa98c4292e5bf04bf968363666cbb8734b85a026 /parsing/g_proofs.ml4 | |
| parent | 2630af30aa52c71e4372215d4180a9e06107abba (diff) | |
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
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 31 |
1 files changed, 18 insertions, 13 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 *) |