diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 30 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 33 insertions, 7 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 430d18893a..e393c2bbfc 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -21,6 +21,24 @@ let thm_token = G_vernac.thm_token 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: hint command; @@ -51,9 +69,15 @@ GEXTEND Gram | 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)) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 595a60f335..feaef31619 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -12,10 +12,10 @@ open Pp open CErrors open Util open Names +open Vernacexpr open Constrexpr open Constrexpr_ops open Extend -open Vernacexpr open Decl_kinds open Declarations open Misctypes @@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl; + record_field decl_notation rec_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -557,8 +557,8 @@ GEXTEND Gram [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] ; with_declaration: - [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> - CWith_Definition (fqid,c) + [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> + CWith_Definition (fqid,udecl,c) | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> CWith_Module (fqid,qid) ] ] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9aae251f1a..258c4bb11c 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -442,6 +442,7 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" + let univ_decl = Gram.entry_create "Prim.univ_decl" let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8592968dc1..e66aa4ade8 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -198,6 +198,7 @@ module Prim : val ident : Id.t Gram.entry val name : lname Gram.entry val identref : lident Gram.entry + val univ_decl : universe_decl_expr Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : lident Gram.entry |