aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_proofs.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r--parsing/g_proofs.ml4120
1 files changed, 60 insertions, 60 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index c1b0c96604..d176a05aaf 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,76 +34,76 @@ GEXTEND Gram
<:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
;
command:
- [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
- | IDENT "Goal"; "." -> <:ast< (GOAL) >>
- | "Proof"; "." -> <:ast< (GOAL) >>
- | IDENT "Begin"; "." -> <:ast< (GOAL) >>
- | IDENT "Abort"; "." -> <:ast< (ABORT) >>
- | "Qed"; "." -> <:ast< (SaveNamed) >>
- | IDENT "Save"; "." -> <:ast< (SaveNamed) >>
- | IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
- | IDENT "Defined"; id = identarg; "." -> <:ast< (DefinedAnonymous $id) >>
- | IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
+ [ [ IDENT "Goal"; c = constrarg -> <:ast< (GOAL $c) >>
+ | IDENT "Goal" -> <:ast< (GOAL) >>
+ | "Proof" -> <:ast< (GOAL) >>
+ | IDENT "Begin" -> <:ast< (GOAL) >>
+ | IDENT "Abort" -> <:ast< (ABORT) >>
+ | "Qed" -> <:ast< (SaveNamed) >>
+ | IDENT "Save" -> <:ast< (SaveNamed) >>
+ | IDENT "Defined" -> <:ast< (DefinedNamed) >>
+ | IDENT "Defined"; id = identarg -> <:ast< (DefinedAnonymous $id) >>
+ | IDENT "Save"; IDENT "Remark"; id = identarg ->
<:ast< (SaveAnonymousRmk $id) >>
- | IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
+ | IDENT "Save"; IDENT "Theorem"; id = identarg ->
<:ast< (SaveAnonymousThm $id) >>
- | IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymous $id) >>
- | IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
- | IDENT "Resume"; "." -> <:ast< (RESUME) >>
- | IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
- | IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
- | IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
- | IDENT "Restart"; "." -> <:ast< (RESTART) >>
- | "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >>
- | IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
- | IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
- | IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
- | IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
+ | IDENT "Save"; id = identarg -> <:ast< (SaveAnonymous $id) >>
+ | IDENT "Suspend" -> <:ast< (SUSPEND) >>
+ | IDENT "Resume" -> <:ast< (RESUME) >>
+ | IDENT "Resume"; id = identarg -> <:ast< (RESUME $id) >>
+ | IDENT "Abort"; IDENT "All" -> <:ast< (ABORTALL) >>
+ | IDENT "Abort"; id = identarg -> <:ast< (ABORT $id) >>
+ | IDENT "Restart" -> <:ast< (RESTART) >>
+ | "Proof"; c = constrarg -> <:ast< (PROOF $c) >>
+ | IDENT "Undo" -> <:ast< (UNDO 1) >>
+ | IDENT "Undo"; n = numarg -> <:ast< (UNDO $n) >>
+ | IDENT "Show"; n = numarg -> <:ast< (SHOW $n) >>
+ | IDENT "Show"; IDENT "Implicits"; n = numarg ->
<:ast< (SHOWIMPL $n) >>
- | IDENT "Focus"; "." -> <:ast< (FOCUS) >>
- | IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
- | IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
- | IDENT "Show"; "." -> <:ast< (SHOW) >>
- | IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
- | IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
- | IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
- | IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
- | IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
+ | IDENT "Focus" -> <:ast< (FOCUS) >>
+ | IDENT "Focus"; n = numarg -> <:ast< (FOCUS $n) >>
+ | IDENT "Unfocus" -> <:ast< (UNFOCUS) >>
+ | IDENT "Show" -> <:ast< (SHOW) >>
+ | IDENT "Show"; IDENT "Implicits" -> <:ast< (SHOWIMPL) >>
+ | IDENT "Show"; IDENT "Node" -> <:ast< (ShowNode) >>
+ | IDENT "Show"; IDENT "Script" -> <:ast< (ShowScript) >>
+ | IDENT "Show"; IDENT "Existentials" -> <:ast< (ShowEx) >>
+ | IDENT "Existential"; n = numarg; ":="; c = constrarg ->
<:ast< (EXISTENTIAL $n $c) >>
| IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
- c2 = Constr.constr; "." ->
+ c2 = Constr.constr ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
| IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
- c1 = Constr.constr; "." ->
+ c1 = Constr.constr ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
- | IDENT "Explain"; "Proof"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; l = numarg_list ->
<:ast< (ExplainProof ($LIST $l)) >>
- | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
+ | IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list ->
<:ast< (ExplainProofTree ($LIST $l)) >>
- | IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
- | IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
- | IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
- | IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
- | IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
- | IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
- | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
- | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
+ | IDENT "Go"; n = numarg -> <:ast< (Go $n) >>
+ | IDENT "Go"; IDENT "top" -> <:ast< (Go "top") >>
+ | IDENT "Go"; IDENT "prev" -> <:ast< (Go "prev") >>
+ | IDENT "Go"; IDENT "next" -> <:ast< (Go "next") >>
+ | IDENT "Show"; "Proof" -> <:ast< (ShowProof) >>
+ | IDENT "Guarded" -> <:ast< (CheckGuard) >>
+ | IDENT "Show"; IDENT "Tree" -> <:ast< (ShowTree) >>
+ | IDENT "Show"; IDENT "Conjectures" -> <:ast< (ShowProofs) >>
(* Definitions for tactics *)
- | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic;
- "." -> <:ast<(TACDEF $name (AST $body))>>
+ | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic
+ -> <:ast<(TACDEF $name (AST $body))>>
| deftok; "Definition"; name=identarg; largs=LIST1 input_fun;
- ":="; body=Tactic.tactic; "." ->
+ ":="; body=Tactic.tactic ->
<:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
- | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ; "." ->
+ | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ->
(match vc with
Coqast.Node(_,"RECCLAUSE",nme::tl) ->
<:ast<(TACDEF $nme (AST (REC $vc)))>>
|_ ->
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 "And"; vcl=LIST1 vrec_clause SEP IDENT "And" ->
let nvcl=
List.fold_right
(fun e b -> match e with
@@ -118,36 +118,36 @@ GEXTEND Gram
(* Hints for Auto and EAuto *)
| IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
- IDENT "Resolve"; c = constrarg; "." ->
+ IDENT "Resolve"; c = constrarg ->
<:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Immediate"; c = constrarg; "." ->
+ IDENT "Immediate"; c = constrarg ->
<:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Unfold"; c = identarg; "." ->
+ IDENT "Unfold"; c = identarg ->
<:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Constructors"; c = qualidarg; "." ->
+ IDENT "Constructors"; c = qualidarg ->
<:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
- IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
+ IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg ->
<:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames))
$n $c (TACTIC $tac))>>
| IDENT "Hints"; IDENT "Resolve"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Immediate"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Unfold"; l = ne_qualidarg_list;
- dbnames = opt_identarg_list; "." ->
+ dbnames = opt_identarg_list ->
<:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "HintDestruct";
@@ -155,14 +155,14 @@ GEXTEND Gram
na = identarg;
hyptyp = constrarg;
pri = numarg;
- tac = Prim.astact; "." ->
+ tac = Prim.astact ->
<:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
- | n = numarg; ":"; tac = tacarg; "." ->
+ | n = numarg; ":"; tac = tacarg ->
<:ast< (SOLVE $n (TACTIC $tac)) >>
(*This entry is not commented, only for debug*)
- | IDENT "PrintConstr"; com = constrarg; "." ->
+ | IDENT "PrintConstr"; com = constrarg ->
<:ast< (PrintConstr $com)>>
] ];
END
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 08:32:53 +0000