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.ml498
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 19:14:56 +0000