diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-05 19:45:07 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-05 19:45:07 +0000 |
| commit | beed52ca495d7cceac9abba5722576a6d9f15ed2 (patch) | |
| tree | 13ebe61c6a1f96ac72e6bc8d701d207c644af603 /parsing | |
| parent | 6156db30ff25c13d9b2da8d5d591b4807e408040 (diff) | |
Arite cachee de Match Context + Meta Definition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1236 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1cd140ed6..0ee8c7aec 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -85,20 +85,20 @@ GEXTEND Gram | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >> | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >> -(* Tactic Definition *) +(* Meta Definition *) - |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic; - "." -> <:ast<(TACDEF $name (AST $body))>> - |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun; + |IDENT "Meta"; "Definition"; name=identarg; ":="; body=Tactic.tactic; + "." -> <:ast<(METADEF $name (AST $body))>> + |IDENT "Meta"; "Definition"; name=identarg; largs=LIST1 input_fun; ":="; body=Tactic.tactic; "." -> - <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>> - |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." -> + <:ast<(METADEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>> + |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause ; "." -> (match vc with Coqast.Node(_,"RECCLAUSE",nme::tl) -> - <:ast<(TACDEF $nme (AST (REC $vc)))>> + <:ast<(METADEF $nme (AST (REC $vc)))>> |_ -> anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) - |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause; + |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause; IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." -> let nvcl= List.fold_right @@ -109,7 +109,7 @@ GEXTEND Gram anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">]) (vc::vcl) [] in - <:ast<(TACDEF ($LIST $nvcl))>> + <:ast<(METADEF ($LIST $nvcl))>> (* Hints for Auto and EAuto *) |