summaryrefslogtreecommitdiff
path: root/parsing/g_proofs.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r--parsing/g_proofs.ml495
1 files changed, 41 insertions, 54 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5262b785..886b33e2 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_proofs.ml4,v 1.33.2.1 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_proofs.ml4 7936 2006-01-28 18:36:54Z herbelin $ *)
open Pcoq
open Pp
@@ -18,10 +18,9 @@ open Vernacexpr
open Prim
open Constr
-let thm_token = Gram.Entry.create "vernac:thm_token"
+let thm_token = G_vernac.thm_token
(* Proof commands *)
-if !Options.v7 then
GEXTEND Gram
GLOBAL: command;
@@ -35,27 +34,29 @@ GEXTEND Gram
| ":"; l = LIST1 IDENT -> l ] ]
;
command:
- [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
- | "Proof" -> VernacProof (Tacexpr.TacId "")
- | "Proof"; "with"; ta = tactic -> VernacProof ta
+ [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
+ | IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
+ | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
| IDENT "Abort" -> VernacAbort None
| IDENT "Abort"; IDENT "All" -> VernacAbortAll
| IDENT "Abort"; id = identref -> VernacAbort (Some id)
+ | IDENT "Existential"; n = natural; c = constr_body ->
+ VernacSolveExistential (n,c)
| IDENT "Admitted" -> VernacEndProof Admitted
- | "Qed" -> VernacEndProof (Proved (true,None))
+ | IDENT "Qed" -> VernacEndProof (Proved (true,None))
| IDENT "Save" -> VernacEndProof (Proved (true,None))
- | IDENT "Defined" -> VernacEndProof (Proved (false,None))
- | IDENT "Defined"; id=identref ->
- VernacEndProof (Proved (false,Some (id,None)))
| IDENT "Save"; tok = thm_token; id = identref ->
VernacEndProof (Proved (true,Some (id,Some tok)))
| IDENT "Save"; id = identref ->
VernacEndProof (Proved (true,Some (id,None)))
+ | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+ | IDENT "Defined"; id=identref ->
+ VernacEndProof (Proved (false,Some (id,None)))
| IDENT "Suspend" -> VernacSuspend
| IDENT "Resume" -> VernacResume None
| IDENT "Resume"; id = identref -> VernacResume (Some id)
| IDENT "Restart" -> VernacRestart
- | "Proof"; c = Constr.constr -> VernacExactProof c
+ | IDENT "Proof"; c = lconstr -> VernacExactProof c
| IDENT "Undo" -> VernacUndo 1
| IDENT "Undo"; n = natural -> VernacUndo n
| IDENT "Focus" -> VernacFocus None
@@ -63,20 +64,20 @@ GEXTEND Gram
| IDENT "Unfocus" -> VernacUnfocus
| IDENT "Show" -> VernacShow (ShowGoal None)
| IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
- | IDENT "Show"; IDENT "Implicits"; n = natural ->
- VernacShow (ShowGoalImplicitly (Some n))
- | IDENT "Show"; IDENT "Implicits" -> VernacShow (ShowGoalImplicitly None)
+ | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
+ VernacShow (ShowGoalImplicitly n)
| IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
| IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
| IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
| IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree
| IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
- | IDENT "Show"; "Proof" -> VernacShow ShowProof
+ | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
| IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
| IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
- | IDENT "Explain"; "Proof"; l = LIST0 integer ->
+ | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+ | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
VernacShow (ExplainProof l)
- | IDENT "Explain"; "Proof"; IDENT "Tree"; l = LIST0 integer ->
+ | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer ->
VernacShow (ExplainTree l)
| IDENT "Go"; n = natural -> VernacGo (GoTo n)
| IDENT "Go"; IDENT "top" -> VernacGo GoTop
@@ -84,26 +85,13 @@ GEXTEND Gram
| IDENT "Go"; IDENT "next" -> VernacGo GoNext
| IDENT "Guarded" -> VernacCheckGuard
(* Hints for Auto and EAuto *)
-
- | IDENT "HintDestruct";
- local = locality;
- dloc = destruct_location;
- id = base_ident;
- hyptyp = Constr.constr_pattern;
- pri = natural;
- "["; tac = tactic; "]" ->
- VernacHints(local,[],HintsDestruct (id,pri,dloc,hyptyp,tac))
-
- | IDENT "Hint"; local = locality; hintname = base_ident;
- dbnames = opt_hintbases; ":="; h = hint
- -> VernacHints (local,dbnames, h hintname)
-
- | IDENT "Hints"; local = locality;
- (dbnames,h) = hints -> VernacHints (local,dbnames, h)
+ | IDENT "Hint"; local = locality; h = hint;
+ dbnames = opt_hintbases ->
+ VernacHints (local,dbnames, h)
(*This entry is not commented, only for debug*)
- | IDENT "PrintConstr"; c = Constr.constr ->
+ | IDENT "PrintConstr"; c = constr ->
VernacExtend ("PrintConstr",
[Genarg.in_gen Genarg.rawwit_constr c])
] ];
@@ -112,24 +100,23 @@ GEXTEND Gram
[ [ IDENT "Local" -> true | -> false ] ]
;
hint:
- [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
- | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
- | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
- | IDENT "Constructors"; c = global -> fun n ->
- HintsConstructors (Some n,[c])
- | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
- fun name -> HintsExtern (Some name,n,c,tac) ] ]
- ;
- hints:
- [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
- (dbnames,
- HintsResolve
- (List.map (fun qid -> (None, CAppExpl(loc,(None,qid),[]))) l))
- | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
- (dbnames,
- HintsImmediate
- (List.map (fun qid-> (None, CAppExpl (loc,(None,qid),[]))) l))
- | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
- (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
+ [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+ | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+ | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
+ | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
+ | IDENT "Extern"; n = natural; c = constr_pattern ; "=>";
+ tac = tactic ->
+ HintsExtern (n,c,tac)
+ | IDENT "Destruct";
+ id = ident; ":=";
+ pri = natural;
+ dloc = destruct_location;
+ hyptyp = constr_pattern;
+ "=>"; tac = tactic ->
+ HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
;
- END
+ constr_body:
+ [ [ ":="; c = lconstr -> c
+ | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
+ ;
+END
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 09:01:31 +0000