diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/attributes.ml | 22 | ||||
| -rw-r--r-- | vernac/attributes.mli | 6 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 67 | ||||
| -rw-r--r-- | vernac/egramml.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 14 | ||||
| -rw-r--r-- | vernac/mltop.ml | 4 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 4 |
10 files changed, 57 insertions, 68 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 194308b77f..7213ba4829 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -163,23 +163,7 @@ let program = let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" -let warn_unqualified_univ_attr = - CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated" - (fun key -> Pp.(str "Attribute " ++ str key ++ - str " should be qualified as \"universes("++str key++str")\".")) - let ukey = "universes" -let universe_transform ~warn_unqualified : unit attribute = - fun atts -> - let atts = List.map (fun (key,_ as att) -> - match key with - | "polymorphic" | "monomorphic" - | "template" | "notemplate" -> - if warn_unqualified then warn_unqualified_univ_attr key; - ukey, VernacFlagList [att] - | _ -> att) atts - in - atts, () let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] let is_universe_polymorphism = @@ -198,16 +182,10 @@ let polymorphic_base = | Some b -> return b | None -> return (is_universe_polymorphism()) -let polymorphic_nowarn = - universe_transform ~warn_unqualified:false >> - qualify_attribute ukey polymorphic_base - let template = - universe_transform ~warn_unqualified:true >> qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") let polymorphic = - universe_transform ~warn_unqualified:true >> qualify_attribute ukey polymorphic_base let deprecation_parser : Deprecation.t key_parser = fun orig args -> diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 0074db66d3..7ecb7e4fb0 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -114,10 +114,6 @@ val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute val vernac_polymorphic_flag : vernac_flag val vernac_monomorphic_flag : vernac_flag -(** For the stm, do not use! *) - -val polymorphic_nowarn : bool attribute - -(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *) +(** For internal use. *) val universe_polymorphism_option_name : string list val is_universe_polymorphism : unit -> bool diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 72e6d41969..ead86bd12f 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -96,38 +96,38 @@ let create_pos = function let find_position_gen current ensure assoc lev = match lev with | None -> - current, (None, None, None, None) + current, (None, None, None, None) | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = add_level None current in - let assoc = create_assoc assoc in - begin match !init with + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = add_level None current in + let assoc = create_assoc assoc in + begin match !init with | None -> (* Create the entry *) - updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) - end - with - (* Nothing has changed *) - Exit -> - (* Just inherit the existing associativity and name (None) *) - current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) + updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init) + end + with + (* Nothing has changed *) + Exit -> + (* Just inherit the existing associativity and name (None) *) + current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None) let rec list_mem_assoc_triple x = function | [] -> false @@ -505,7 +505,11 @@ let target_to_bool : type r. r target -> bool = function let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) = let empty = (pos, [(name, p4assoc, [])]) in - ExtendRule (target_entry where forpat, reinit, empty) + match reinit with + | None -> + ExtendRule (target_entry where forpat, empty) + | Some reinit -> + ExtendRuleReinit (target_entry where forpat, reinit, empty) let different_levels (custom,opt_level) (custom',string_level) = match opt_level with @@ -552,7 +556,12 @@ let extend_constr state forpat ng = | MayRecRNo symbs -> Rule (symbs, act) | MayRecRMay symbs -> Rule (symbs, act) in name, p4assoc, [r] in - let r = ExtendRule (entry, reinit, (pos, [rule])) in + let r = match reinit with + | None -> + ExtendRule (entry, (pos, [rule])) + | Some reinit -> + ExtendRuleReinit (entry, reinit, (pos, [rule])) + in (accu @ empty_rules @ [r], state) in List.fold_left fold ([], state) ng.notgram_prods diff --git a/vernac/egramml.ml b/vernac/egramml.ml index 62eb561f3c..2b1d99c7a9 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl = vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s, l) in let rules = [make_rule mkact gl] in - grammar_extend nt None (None, [None, None, rules]) + grammar_extend nt (None, [None, None, rules]) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d597707d12..def4ed942a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,7 +402,7 @@ GRAMMAR EXTEND Gram ; constructor_list_or_record_decl: [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l } - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + | id = identref ; c = constructor_type; "|"; l = LIST1 constructor SEP "|" -> { Constructors ((c id)::l) } | id = identref ; c = constructor_type -> { Constructors [ c id ] } | cstr = identref; "{"; fs = record_fields; "}" -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f6f6c4f1eb..07ec6ca1ba 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1356,6 +1356,12 @@ let explain_prim_token_notation_error kind env sigma = function Nota: explain_exn does NOT end with a newline anymore! *) +exception Unhandled + +let wrap_unhandled f e = + try Some (f e) + with Unhandled -> None + let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") @@ -1366,9 +1372,9 @@ let explain_exn_default = function | CErrors.Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Otherwise, not handled here *) - | _ -> raise CErrors.Unhandled + | _ -> raise Unhandled -let _ = CErrors.register_handler explain_exn_default +let _ = CErrors.register_handler (wrap_unhandled explain_exn_default) let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> @@ -1409,6 +1415,6 @@ let rec vernac_interp_error_handler = function | Logic_monad.TacticFailure e -> vernac_interp_error_handler e | _ -> - raise CErrors.Unhandled + raise Unhandled -let _ = CErrors.register_handler vernac_interp_error_handler +let _ = CErrors.register_handler (wrap_unhandled vernac_interp_error_handler) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index ab9d008659..5046248e11 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -99,9 +99,9 @@ let ocaml_toploop () = *) let _ = CErrors.register_handler (function | Dynlink.Error e -> - hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) + Some (hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))) | _ -> - raise CErrors.Unhandled + None ) let ml_load s = diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 826e88cabf..2425f3d6c1 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -58,7 +58,7 @@ module Vernac_ = Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); Rule (Next (Stop, Aentry vernac_control), act_vernac); ] in - Pcoq.grammar_extend main_entry None (None, [None, None, rule]) + Pcoq.grammar_extend main_entry (None, [None, None, rule]) let select_tactic_entry spec = match spec with diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e29086d726..f41df06f85 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -254,7 +254,7 @@ let vernac_argument_extend ~name arg = e | Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in e in let pr = arg.arg_printer in diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 80b72225f0..3c70961e06 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,8 +124,8 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - Pp.(str "No focused proof (No proof-editing in progress).") - | _ -> raise CErrors.Unhandled + Some (Pp.(str "No focused proof (No proof-editing in progress).")) + | _ -> None end open Lemmas |