diff options
Diffstat (limited to 'parsing/g_proofsnew.ml4')
| -rw-r--r-- | parsing/g_proofsnew.ml4 | 126 |
1 files changed, 0 insertions, 126 deletions
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 deleted file mode 100644 index 04bf7a8b..00000000 --- a/parsing/g_proofsnew.ml4 +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* 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 |