diff options
Diffstat (limited to 'parsing/g_proofsnew.ml4')
| -rw-r--r-- | parsing/g_proofsnew.ml4 | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 new file mode 100644 index 00000000..04bf7a8b --- /dev/null +++ b/parsing/g_proofsnew.ml4 @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_proofsnew.ml4,v 1.9.2.1 2004/07/16 19:30:39 herbelin Exp $ *) + +open Pcoq +open Pp +open Tactic +open Util +open Vernac_ +open Topconstr +open Vernacexpr +open Prim +open Constr + +let thm_token = G_vernacnew.thm_token + +(* Proof commands *) +if not !Options.v7 then +GEXTEND Gram + GLOBAL: command; + + destruct_location : + [ [ IDENT "Conclusion" -> Tacexpr.ConclLocation () + | discard = [ IDENT "Discardable" -> true | -> false ]; "Hypothesis" + -> Tacexpr.HypLocation discard ] ] + ; + opt_hintbases: + [ [ -> [] + | ":"; l = LIST1 IDENT -> l ] ] + ; + command: + [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c + | IDENT "Proof" -> VernacNop + | 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 + | IDENT "Qed" -> VernacEndProof (Proved (true,None)) + | IDENT "Save" -> VernacEndProof (Proved (true,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 + | IDENT "Proof"; c = Constr.lconstr -> VernacExactProof c + | IDENT "Undo" -> VernacUndo 1 + | IDENT "Undo"; n = natural -> VernacUndo n + | IDENT "Focus" -> VernacFocus None + | IDENT "Focus"; n = natural -> VernacFocus (Some n) + | IDENT "Unfocus" -> VernacUnfocus + | IDENT "Show" -> VernacShow (ShowGoal None) + | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n)) + | 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"; IDENT "Proof" -> VernacShow ShowProof + | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) + | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) + | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> + VernacShow (ExplainProof l) + | 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 + | IDENT "Go"; IDENT "prev" -> VernacGo GoPrev + | IDENT "Go"; IDENT "next" -> VernacGo GoNext + | IDENT "Guarded" -> VernacCheckGuard +(* Hints for Auto and EAuto *) + | 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 -> + VernacExtend ("PrintConstr", + [Genarg.in_gen Genarg.rawwit_constr c]) + ] ]; + + locality: + [ [ IDENT "Local" -> true | -> false ] ] + ; + hint: + [ [ IDENT "Resolve"; lc = LIST1 Constr.constr -> + HintsResolve (List.map (fun c -> (None, c)) lc) + | IDENT "Immediate"; lc = LIST1 Constr.constr -> + HintsImmediate (List.map (fun c -> (None,c)) lc) + | IDENT "Unfold"; lqid = LIST1 global -> + HintsUnfold (List.map (fun g -> (None,g)) lqid) + | IDENT "Constructors"; lc = LIST1 global -> + HintsConstructors (None,lc) + | IDENT "Extern"; n = natural; c = Constr.constr_pattern ; "=>"; + tac = tactic -> + HintsExtern (None,n,c,tac) + | IDENT"Destruct"; + id = base_ident; ":="; + pri = natural; + dloc = destruct_location; + hyptyp = Constr.constr_pattern; + "=>"; tac = tactic -> + HintsDestruct(id,pri,dloc,hyptyp,tac) ] ] + ; + constr_body: + [ [ ":="; c = lconstr -> c + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,t) ] ] + ; +END |