diff options
Diffstat (limited to 'parsing/g_proofs.ml4')
-rw-r--r-- | parsing/g_proofs.ml4 | 98 |
1 files changed, 46 insertions, 52 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 70c5d5d8..e393c2bb 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,50 +1,57 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Compat open Constrexpr open Vernacexpr open Misctypes -open Tok open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ let thm_token = G_vernac.thm_token -let hint_proof_using e = function - | Some _ as x -> x - | None -> match Proof_using.get_default_proof_using () with - | None -> None - | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s))) +let hint = Gram.entry_create "hint" + +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") (* Proof commands *) GEXTEND Gram - GLOBAL: command; + GLOBAL: hint command; opt_hintbases: [ [ -> [] | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] ; command: - [ [ IDENT "Goal"; c = lconstr -> VernacGoal c - | IDENT "Proof" -> - VernacProof (None,hint_proof_using G_vernac.section_subset_expr None) + [ [ IDENT "Goal"; c = lconstr -> + VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) + | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn - | IDENT "Proof"; "with"; ta = tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - VernacProof (Some ta,hint_proof_using G_vernac.section_subset_expr l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - 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 @@ -52,44 +59,37 @@ GEXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) - | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," -> - VernacEndProof (Proved (Opaque (Some l),None)) - | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None)) - | IDENT "Save"; tok = thm_token; id = identref -> - VernacEndProof (Proved (Opaque None,Some (id,Some tok))) + | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque None,Some (id,None))) + VernacEndProof (Proved (Opaque, Some id)) | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (Transparent,Some (id,None))) + VernacEndProof (Proved (Transparent,Some id)) | IDENT "Restart" -> VernacRestart | 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 "Focus" -> + warn_deprecated_focus ~loc:!@loc (); + VernacFocus None + | IDENT "Focus"; n = natural -> + warn_deprecated_focus_n n ~loc:!@loc (); + VernacFocus (Some n) + | IDENT "Unfocus" -> + warn_deprecated_unfocus ~loc:!@loc (); + VernacUnfocus | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal"))) - | IDENT "Show"; IDENT "Goal"; n = string -> - VernacShow (ShowGoal (GoalUid 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 "Universes" -> VernacShow ShowUniverses - | 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 "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) - | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; @@ -97,19 +97,16 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; local = obsolete_locality; h = hint; + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> - VernacHints (local,dbnames, h) + VernacHints (dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info; dbnames = opt_hintbases -> - VernacHints (false,dbnames, + VernacHints (dbnames, HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; - obsolete_locality: - [ [ IDENT "Local" -> true | -> false ] ] - ; reference_or_constr: [ [ r = global -> HintsReference r | c = constr -> HintsConstr c ] ] @@ -122,14 +119,11 @@ GEXTEND Gram | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid - | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc - | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; - tac = tactic -> - HintsExtern (n,c,tac) ] ] + | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ] ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] ; mode: [ [ l = LIST1 [ "+" -> ModeInput |