diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 70 |
1 files changed, 24 insertions, 46 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f1dad3b2..8a6f67c4 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,16 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo" i*) - -(* $Id: g_proofs.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - - open Pcoq open Pp open Tactic @@ -20,6 +15,7 @@ open Topconstr open Vernacexpr open Prim open Constr +open Tok let thm_token = G_vernac.thm_token @@ -27,19 +23,21 @@ let thm_token = G_vernac.thm_token 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 ] ] + | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) - | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta + | IDENT "Proof" -> VernacProof (None,None) + | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn + | IDENT "Proof"; "with"; ta = tactic; + l = OPT [ "using"; l = LIST0 identref -> l ] -> + VernacProof (Some ta, l) + | IDENT "Proof"; "using"; l = LIST0 identref; + ta = OPT [ "with"; ta = tactic -> ta ] -> + VernacProof (ta,Some l) + | IDENT "Proof"; c = lconstr -> VernacExactProof c | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll | IDENT "Abort"; id = identref -> VernacAbort (Some id) @@ -55,19 +53,18 @@ GEXTEND Gram | 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 = lconstr -> VernacExactProof c | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo 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 "Unfocused" -> VernacUnfocused + | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) + | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; IDENT "Goal"; n = string -> + VernacShow (ShowGoal (GoalId n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode @@ -80,34 +77,22 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis - | 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 *) + (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> VernacCreateHintDb (use_module_locality (), id, b) + | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> + VernacRemoveHints (use_module_locality (), dbnames, ids) | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> VernacHints (enforce_module_locality local,dbnames, h) - -(* Declare "Resolve" directly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) + (* Declare "Resolve" explicitly so as to be able to later extend with + "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; dbnames = opt_hintbases -> VernacHints (use_module_locality (),dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) - -(*This entry is not commented, only for debug*) - | IDENT "PrintConstr"; c = constr -> - VernacExtend ("PrintConstr", - [Genarg.in_gen Genarg.rawwit_constr c]) ] ]; obsolete_locality: @@ -123,17 +108,10 @@ GEXTEND Gram | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT 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) ] ] + HintsExtern (n,c,tac) ] ] ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv (Term.DEFAULTcast,t)) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ] ; END |