aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-05 19:45:07 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-05 19:45:07 +0000
commitbeed52ca495d7cceac9abba5722576a6d9f15ed2 (patch)
tree13ebe61c6a1f96ac72e6bc8d701d207c644af603 /parsing
parent6156db30ff25c13d9b2da8d5d591b4807e408040 (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.ml418
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 *)