diff options
Diffstat (limited to 'library')
42 files changed, 203 insertions, 136 deletions
diff --git a/library/declare.ml b/library/declare.ml index c1697a434a..b0df32b8de 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -32,6 +32,14 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) +(** XML output hooks *) + +let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () +let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () +let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -83,6 +91,7 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); + if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -149,7 +158,7 @@ let cache_constant ((sp,kn), obj) = assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in - add_section_constant (cst.const_proj <> None) kn' cst.const_hyps; + add_section_constant cst.const_polymorphic kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -216,6 +225,7 @@ let declare_constant_common id cst = let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) @@ -257,6 +267,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_was_seff = false; } in let kn = declare_constant_common id cst in + let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn let declare_definition ?(internal=UserIndividualRequest) @@ -314,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn kn' mind.mind_hyps; + add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -365,8 +376,9 @@ let declare_projections mind = let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns; true - | Some None | None -> false + assert(eq_constant kn kn')) kns; true,true + | Some None -> true,false + | None -> false,false (* for initial declaration *) let declare_mind mie = @@ -375,9 +387,10 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mind in + let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; + if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) @@ -385,7 +398,7 @@ let declare_mind mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -400,7 +413,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -410,10 +423,13 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) diff --git a/library/declare.mli b/library/declare.mli index c6119a58ac..8dd24d2780 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -71,6 +71,11 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool +(** Hooks for XML output *) +val xml_declare_variable : (object_name -> unit) Hook.t +val xml_declare_constant : (internal_flag * constant -> unit) Hook.t +val xml_declare_inductive : (bool * object_name -> unit) Hook.t + (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index d8c5ab5e74..f3f734aa09 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -557,6 +557,17 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" +(** XML output hooks *) + +let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () +let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () +let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () +let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () +let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () +let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -578,7 +589,9 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module) mp; + mp let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in @@ -617,6 +630,7 @@ let end_module () = assert (ModPath.equal (mp_of_kn (snd newoname)) mp); Lib.add_frozen_state () (* to prevent recaching *); + if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -628,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs = let env = Global.env () in let mty_entry_o, subs, inl_res = match res with | Enforce (mty,ann) -> - Some (fst (interp_modast env ModType mty)), [], inl2intopt ann + let inl = inl2intopt ann in + let mte, _ = interp_modast env ModType mty in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in + Some mte, [], inl | Check mtys -> None, build_subtypes interp_modast env mp arg_entries_r mtys, default_inline () @@ -666,6 +684,7 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); + if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -682,7 +701,9 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module_type) mp; + mp let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in @@ -699,6 +720,7 @@ let end_modtype () = assert (ModPath.equal (mp_of_kn (snd oname)) mp); Lib.add_frozen_state ()(* to prevent recaching *); + if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -709,7 +731,10 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let arg_entries_r = intern_args interp_modast args in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let entry = params, fst (interp_modast env ModType mty) in + let mte, _ = interp_modast env ModType mty in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in + let entry = params, mte in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in @@ -729,6 +754,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); + if_xml (Hook.get f_xml_declare_module_type) mp; mp end diff --git a/library/declaremods.mli b/library/declaremods.mli index 319d168d05..2b440c087a 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -63,6 +63,13 @@ val start_modtype : val end_modtype : unit -> module_path +(** Hooks for XML output *) +val xml_declare_module : (module_path -> unit) Hook.t +val xml_start_module : (module_path -> unit) Hook.t +val xml_end_module : (module_path -> unit) Hook.t +val xml_declare_module_type : (module_path -> unit) Hook.t +val xml_start_module_type : (module_path -> unit) Hook.t +val xml_end_module_type : (module_path -> unit) Hook.t (** {6 Libraries i.e. modules on disk } *) diff --git a/library/decls.ml b/library/decls.ml index b5f9143b8a..6e21880f1f 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,16 +46,20 @@ let constant_kind kn = Cmap.find kn !csttab (** Miscellaneous functions. *) +open Context.Named.Declaration + let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right - (fun (id,c,t as d) signv -> - let d = if variable_opacity id then (id,None,t) else d in + (fun d signv -> + let id = get_id d in + let d = if variable_opacity id then LocalAssum (id, get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val let last_section_hyps dir = Context.Named.fold_outside - (fun (id,_,_) sec_ids -> + (fun d sec_ids -> + let id = get_id d in try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) diff --git a/library/decls.mli b/library/decls.mli index ac0d907d87..1ca7f89469 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index e4280334dc..cea1fd7d6e 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 736892016b..ea4a9424e5 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/global.ml b/library/global.ml index 4cffd6b7e3..2398e92b03 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/global.mli b/library/global.mli index d6547105d4..bf653307c4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/globnames.ml b/library/globnames.ml index 2d6afc8577..bec463ecf2 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y = let global_ord_gen ord_cst ord_ind ord_cons x y = if x == y then 0 else match x, y with + | VarRef v1, VarRef v2 -> Id.compare v1 v2 + | VarRef _, _ -> -1 + | _, VarRef _ -> 1 | ConstRef cx, ConstRef cy -> ord_cst cx cy + | ConstRef _, _ -> -1 + | _, ConstRef _ -> 1 | IndRef indx, IndRef indy -> ord_ind indx indy + | IndRef _, _ -> -1 + | _ , IndRef _ -> 1 | ConstructRef consx, ConstructRef consy -> ord_cons consx consy - | VarRef v1, VarRef v2 -> Id.compare v1 v2 - - | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1 - | ConstRef _, VarRef _ -> 1 - | ConstRef _, (IndRef _ | ConstructRef _) -> -1 - | IndRef _, (VarRef _ | ConstRef _) -> 1 - | IndRef _, ConstructRef _ -> -1 - | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1 let global_hash_gen hash_cst hash_ind hash_cons gr = let open Hashset.Combine in diff --git a/library/globnames.mli b/library/globnames.mli index a401046b49..f4956e3df2 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/goptions.ml b/library/goptions.ml index 30d195f83c..4aa3a2a21d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -108,7 +108,8 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - pp (str table_name ++ + Feedback.msg_notice + (str table_name ++ (hov 0 (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold @@ -122,7 +123,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg_info (A.member_message y answer) + Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -271,7 +272,7 @@ let declare_option cast uncast in let warn () = if depr then - msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") in let cread () = cast (read ()) in let cwrite v = warn (); write (uncast v) in @@ -346,12 +347,12 @@ let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + with UserError (_,s) -> Feedback.msg_warning s let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None @@ -375,9 +376,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/goptions.mli b/library/goptions.mli index 25b5315c2a..26864503b1 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/heads.ml b/library/heads.ml index 73d2aa053f..4c9b789769 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,6 +15,7 @@ open Environ open Globnames open Libobject open Lib +open Context.Named.Declaration (** Characterization of the head of a term *) @@ -63,9 +64,9 @@ let kind_of_head env t = (try on_subterm k l b (variable_head id) with Not_found -> (* a goal variable *) - match pi2 (lookup_named id env) with - | Some c -> aux k l c b - | None -> NotImmediatelyComputableHead) + match lookup_named id env with + | LocalDef (_,c,_) -> aux k l c b + | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) with Not_found -> @@ -132,8 +133,8 @@ let compute_head = function | None -> RigidHead (RigidParameter cst) | Some c -> kind_of_head env c) | EvalVarRef id -> - (match pi2 (Global.lookup_named id) with - | Some c when not (Decls.variable_opacity id) -> + (match Global.lookup_named id with + | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c | _ -> RigidHead (RigidVar id)) diff --git a/library/heads.mli b/library/heads.mli index 52f43824fd..5acf5f54f7 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/impargs.ml b/library/impargs.ml index d15a02fea2..4e344a9543 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -165,6 +165,7 @@ let update pos rig (na,st) = (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env bound depth f = + let open Context.Named.Declaration in match kind_of_term f with | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true @@ -173,8 +174,7 @@ let is_flexible_reference env bound depth f = let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> - let (_, value, _) = Environ.lookup_named id env in - begin match value with None -> false | _ -> true end + Environ.lookup_named id env |> is_local_def | Ind _ | Construct _ -> false | _ -> true @@ -234,13 +234,14 @@ let find_displayed_name_in all avoid na (_,b as envnames_b) = let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in + let open Context.Rel.Declaration in let rec aux env avoid n names t = let t = whd_betadeltaiota env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1)) - (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b) + (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) | _ -> rigid := is_rigid_head t; let names = List.rev names in @@ -252,7 +253,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = match kind_of_term (whd_betadeltaiota env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in - let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in + let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in !rigid, Array.to_list v | _ -> true, [] @@ -427,7 +428,7 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = @@ -449,8 +450,8 @@ let compute_all_mib_implicits flags manual kn = let compute_var_implicits flags manual id = let env = Global.env () in - let (_,_,ty) = lookup_named id env in - compute_semi_auto_implicits env flags manual ty + let open Context.Named.Declaration in + compute_semi_auto_implicits env flags manual (get_type (lookup_named id env)) (* Implicits of a global reference. *) diff --git a/library/impargs.mli b/library/impargs.mli index 30f2e30f97..34e529ca2c 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/keys.ml b/library/keys.ml index e30cf67175..057dc3b65d 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/keys.mli b/library/keys.mli index bfbb4c58f6..69668590d6 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/kindops.ml b/library/kindops.ml index 5604864737..c634193da8 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/kindops.mli b/library/kindops.mli index cd2e39cf85..3e95eaa7d9 100644 --- a/library/kindops.mli +++ b/library/kindops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/lib.ml b/library/lib.ml index 297441e6e2..f8bb6bac59 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -408,21 +408,30 @@ let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab +let check_same_poly p vars = + let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in + if List.exists pred vars then + error "Cannot mix universe polymorphic and monomorphic declarations in sections." + let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + check_same_poly poly vars; + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := (Context ctx :: vars,repl,abs)::sl + check_same_poly true vars; + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = + let open Context.Named.Declaration in let rec aux = function - | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) -> + let (id',b,t) = to_tuple decl in let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r | (Variable (_,_,poly,ctx)::idl,hyps) -> @@ -441,12 +450,16 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx +let named_of_variable_context ctx = let open Context.Named.Declaration in + List.map (function id,_,None,t -> LocalAssum (id,t) + | id,_,Some b,t -> LocalDef (id,b,t)) + ctx -let add_section_replacement f g hyps = +let add_section_replacement f g poly hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> + let () = check_same_poly poly vars in let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in @@ -454,13 +467,13 @@ let add_section_replacement f g hyps = sectab := (vars,f (Univ.UContext.instance ctx,args) exps, g (sechyps,subst,ctx) abs)::sl -let add_section_kn kn = +let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f + add_section_replacement f f poly -let add_section_constant is_projection kn = +let add_section_constant poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f + add_section_replacement f f poly let replacement_context () = pi2 (List.hd !sectab) @@ -497,6 +510,10 @@ let full_section_segment_of_constant con = (*************) (* Sections. *) +(* XML output hooks *) +let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () +let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () + let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = add_dirpath_suffix olddir id in @@ -508,6 +525,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; + if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -536,6 +554,7 @@ let close_section () = let full_olddir = fst !path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); + if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index 874fc89fb4..e2e71ac90f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -157,6 +157,10 @@ val unfreeze : frozen -> unit val init : unit -> unit +(** XML output hooks *) +val xml_open_section : (Names.Id.t -> unit) Hook.t +val xml_close_section : (Names.Id.t -> unit) Hook.t + (** {6 Section management for discharge } *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types @@ -174,9 +178,10 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit -val add_section_constant : bool (* is_projection *) -> +val add_section_constant : Decl_kinds.polymorphic -> Names.constant -> Context.Named.t -> unit -val add_section_kn : Names.mutual_inductive -> Context.Named.t -> unit +val add_section_kn : Decl_kinds.polymorphic -> + Names.mutual_inductive -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) diff --git a/library/libnames.ml b/library/libnames.ml index 36b46ca498..99ff2f2fb4 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/libnames.mli b/library/libnames.mli index c72f517532..58d1da9d64 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/libobject.ml b/library/libobject.ml index f0d281a2dd..b12d2038ae 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -78,20 +78,9 @@ let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) -let make_dyn (type a) (tag : a Dyn.tag) = - let infun x = Dyn.Dyn (tag, x) in - let outfun : (Dyn.t -> a) = fun dyn -> - let Dyn.Dyn (t, x) = dyn in - match Dyn.eq t tag with - | None -> assert false - | Some Refl -> x - in - (infun, outfun) - let declare_object_full odecl = let na = odecl.object_name in - let tag = Dyn.create na in - let (infun, outfun) = make_dyn tag in + let (infun, outfun) = Dyn.Easy.make_dyn na in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) @@ -144,7 +133,7 @@ let apply_dyn_fun deflt f lobj = Failure "local to_apply_dyn_fun" -> if not (!relax_flag || Hashtbl.mem missing_tab tag) then begin - Pp.msg_warning + Feedback.msg_warning (Pp.str ("Cannot find library functions for an object with tag " ^ tag ^ " (a plugin may be missing)")); Hashtbl.add missing_tab tag () diff --git a/library/libobject.mli b/library/libobject.mli index 12b1a558f8..dbe0de8f8a 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/library.ml b/library/library.ml index db95213fe9..192700be79 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -171,9 +171,8 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - (* This will not produce errors or warnings if the native compiler was - not enabled *) - Nativelib.link_library ~prefix ~dirname ~basename:f + if not Coq_config.no_native_compiler then + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> link m; [libname] @@ -288,7 +287,7 @@ let locate_absolute_library dir = | [] -> raise LibNotFound | [file] -> file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); vi | [vo;vi] -> vo @@ -312,7 +311,7 @@ let locate_qualified_library ?root ?(warn = true) qid = | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ + Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++ str vo ++ str " because it is more recent"); lpath_vi, vi | [lpath_vo, vo; _ ] -> lpath_vo, vo @@ -371,7 +370,7 @@ let access_table what tables dp i = | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let t = try fetch_delayed f with Faulty f -> @@ -449,7 +448,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Pp.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -464,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); + Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); m.library_digests, intern_library_deps (needed, contents) dir m (Some f) and intern_library_deps libs dir m from = @@ -546,6 +545,8 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) +let (f_xml_require, xml_require) = Hook.make ~default:ignore () + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in @@ -559,6 +560,7 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); + if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; add_frozen_state () (* the function called by Vernacentries.vernac_import *) @@ -753,7 +755,7 @@ let save_library_to ?todo dir f otab = error "Could not compile the library to native code." with reraise -> let reraise = Errors.push reraise in - let () = msg_warning (str "Removed file " ++ str f') in + let () = Feedback.msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/library.mli b/library/library.mli index 71aefdbd86..8f5b775d8d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,6 +67,9 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit +(** {6 Hook for the xml exportation of libraries } *) +val xml_require : (DirPath.t -> unit) Hook.t + (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound diff --git a/library/loadpath.ml b/library/loadpath.ml index f77bd1ef53..33c0f41e17 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,7 +72,7 @@ let add_load_path phys_path coq_path ~implicit = let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath old_path ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path) in diff --git a/library/loadpath.mli b/library/loadpath.mli index 732f6349fb..4e79edbdcf 100644 --- a/library/loadpath.mli +++ b/library/loadpath.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nameops.ml b/library/nameops.ml index 418d620c25..71405d0240 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nameops.mli b/library/nameops.mli index de1f99fe0f..39ce409bcf 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nametab.ml b/library/nametab.ml index 621640ef98..db902d625b 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,7 +119,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -155,7 +155,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" + Feedback.msg_warning (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")); tree.path | Nothing @@ -525,7 +525,7 @@ let shortest_qualid_of_tactic kn = let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> - if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e + if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e let global_inductive r = match global r with diff --git a/library/nametab.mli b/library/nametab.mli index e3aeb67579..a8a0572b33 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/states.ml b/library/states.ml index 3cb6da12ec..2e1be764ab 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/states.mli b/library/states.mli index 4d5d63e037..12c71c9991 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/summary.ml b/library/summary.ml index a922e155dd..edea7dbe50 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -22,19 +22,8 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" -let make_dyn (type a) (tag : a Dyn.tag) = - let infun x = Dyn.Dyn (tag, x) in - let outfun : (Dyn.t -> a) = fun dyn -> - let Dyn.Dyn (t, x) = dyn in - match Dyn.eq t tag with - | None -> assert false - | Some Refl -> x - in - (infun, outfun) - let internal_declare_summary hash sumname sdecl = - let tag = Dyn.create (mangle sumname) in - let (infun, outfun) = make_dyn tag in + let (infun, outfun) = Dyn.Easy.make_dyn (mangle sumname) in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in diff --git a/library/summary.mli b/library/summary.mli index a35113fd2e..27889cab27 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/universes.ml b/library/universes.ml index b9b148b57b..c4eb2afcbb 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -954,10 +954,10 @@ let universes_of_constr c = let rec aux s c = match kind_of_term c with | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.union (Instance.levels u) s + LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = univ_of_sort u in - LSet.union (Universe.levels u) s + LSet.fold LSet.add (Universe.levels u) s | _ -> fold_constr aux s c in aux LSet.empty c diff --git a/library/universes.mli b/library/universes.mli index 7b17b88987..53cf5f3844 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |