diff options
| author | delahaye | 2001-01-09 16:30:04 +0000 |
|---|---|---|
| committer | delahaye | 2001-01-09 16:30:04 +0000 |
| commit | 9ede7b4e8319516aee4df9dc0ddfd13040049877 (patch) | |
| tree | b2a61ff2d8aae1049c9315af5023f02196008845 /parsing | |
| parent | dfe152b89af9239899e32b2a31adbfda44af5efe (diff) | |
Meta Definition + Tactic Definition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 0ee8c7aec1..207c624974 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -25,6 +25,10 @@ GEXTEND Gram [ [ -> [] | ":"; l = LIST1 identarg -> l ] ] ; + deftok: + [ [ IDENT "Meta" + | IDENT "Tactic" ] ] + ; vrec_clause: [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr -> <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ] @@ -85,20 +89,20 @@ GEXTEND Gram | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >> | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >> -(* Meta Definition *) +(* Definitions for tactics *) - |IDENT "Meta"; "Definition"; name=identarg; ":="; body=Tactic.tactic; - "." -> <:ast<(METADEF $name (AST $body))>> - |IDENT "Meta"; "Definition"; name=identarg; largs=LIST1 input_fun; + | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic; + "." -> <:ast<(TACDEF $name (AST $body))>> + | deftok; "Definition"; name=identarg; largs=LIST1 input_fun; ":="; body=Tactic.tactic; "." -> - <:ast<(METADEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>> - |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause ; "." -> + <: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<(METADEF $nme (AST (REC $vc)))>> + <:ast<(TACDEF $nme (AST (REC $vc)))>> |_ -> anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) - |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause; + |IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause; IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." -> let nvcl= List.fold_right @@ -109,7 +113,7 @@ GEXTEND Gram anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) (vc::vcl) [] in - <:ast<(METADEF ($LIST $nvcl))>> + <:ast<(TACDEF ($LIST $nvcl))>> (* Hints for Auto and EAuto *) |