From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- library/declare.ml | 23 ++++++++++++++++++----- library/declare.mli | 7 ++++++- library/declaremods.ml | 25 ++++++++++++++++++++++--- library/declaremods.mli | 9 ++++++++- library/decls.ml | 2 +- library/decls.mli | 2 +- library/dischargedhypsmap.ml | 2 +- library/dischargedhypsmap.mli | 2 +- library/global.ml | 6 +++--- library/global.mli | 2 +- library/globnames.ml | 2 +- library/globnames.mli | 2 +- library/goptions.ml | 2 +- library/goptions.mli | 4 ++-- library/heads.ml | 2 +- library/heads.mli | 2 +- library/impargs.ml | 2 +- library/impargs.mli | 2 +- library/keys.ml | 2 +- library/keys.mli | 2 +- library/kindops.ml | 2 +- library/kindops.mli | 2 +- library/lib.ml | 8 +++++++- library/lib.mli | 6 +++++- library/libnames.ml | 2 +- library/libnames.mli | 4 ++-- library/libobject.ml | 2 +- library/libobject.mli | 2 +- library/library.ml | 5 ++++- library/library.mli | 5 ++++- library/loadpath.ml | 2 +- library/loadpath.mli | 2 +- library/nameops.ml | 2 +- library/nameops.mli | 2 +- library/nametab.ml | 2 +- library/nametab.mli | 2 +- library/states.ml | 2 +- library/states.mli | 2 +- library/summary.ml | 2 +- library/summary.mli | 2 +- library/universes.ml | 24 +++++++++++++++--------- library/universes.mli | 2 +- 42 files changed, 126 insertions(+), 60 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 5968fbf3..5f6f0fe4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* () | 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) @@ -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 *) @@ -431,7 +444,7 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set false ctx; + Global.push_context_set p ctx; if p then Lib.add_section_context ctx; Universes.set_global_universe_names glob' diff --git a/library/declare.mli b/library/declare.mli index c6119a58..8dd24d27 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 7f607a51..04348415 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 8d5085f7..0cd4ccb2 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in Inductive.type_of_inductive env (specif, Univ.UContext.instance univs), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = - if mib.mind_polymorphic then mib.mind_universes + if mib.mind_polymorphic then Univ.instantiate_univ_context mib.mind_universes else Univ.UContext.empty in let inst = Univ.UContext.instance univs in diff --git a/library/global.mli b/library/global.mli index 03469bea..9db30c8f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* string option write_fu (** {6 Special functions supposed to be used only in vernacentries.ml } *) -module OptionMap : Map.S with type key = option_name +module OptionMap : CSig.MapS with type key = option_name val get_string_table : option_name -> diff --git a/library/heads.ml b/library/heads.ml index 73d2aa05..8124d347 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index bb883175..29fc7cd2 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 diff --git a/library/libnames.ml b/library/libnames.ml index cdaec6a3..a2f22b2e 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* full_path val string_of_path : full_path -> string val pr_path : full_path -> std_ppcmds -module Spmap : Map.S with type key = full_path +module Spmap : CSig.MapS with type key = full_path val restrict_path : int -> full_path -> full_path diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea..706e3991 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 @@ -568,6 +570,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 *) diff --git a/library/library.mli b/library/library.mli index d5e610dd..25c9604c 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 622d390a..78f8dd25 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs - else + else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs with Option.IsNone -> failwith "") @@ -854,7 +854,7 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - if is_set_minimization () then + if is_set_minimization () && LSet.mem r ctx then (Constraint.add cstr smallles, noneqs) else (smallles, noneqs) else if Level.is_small r then @@ -904,22 +904,28 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> + let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> Constraint.add (canon, Univ.Eq, g) cst) global cstrs in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) rigid + cstrs + in let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in - (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs)) - (ctx, LMap.empty, Constraint.empty) partition + let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, subst, us, cstrs)) + (ctx, LMap.empty, us, Constraint.empty) partition in (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = subst_univs_level_constraints subst noneqs in - let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = diff --git a/library/universes.mli b/library/universes.mli index 45672ef4..edb06dfc 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*