diff options
Diffstat (limited to 'library')
45 files changed, 223 insertions, 152 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 0cb8c7afcf..8787738af9 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/coqlib.mli b/library/coqlib.mli index 716d97c9d0..1e3c37a9ed 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/declare.ml b/library/declare.ml index 7d0edbc8b3..154793a32d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -158,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_polymorphic kn' cst.const_hyps; + add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -325,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 mind.mind_polymorphic kn' mind.mind_hyps; + add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -333,9 +333,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in + let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) + Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -351,11 +351,27 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_polymorphic = false; - mind_entry_universes = Univ.UContext.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; mind_entry_private = None; }) +(* reinfer subtyping constraints for inductive after section is dischared. *) +let infer_inductive_subtyping (pth, mind_ent) = + match mind_ent.mind_entry_universes with + | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> + (pth, mind_ent) + | Cumulative_ind_entry cumi -> + begin + let env = Global.env () in + let env' = + Environ.push_context + (Univ.CumulativityInfo.univ_context cumi) env + in + (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) + let evd = Evd.from_env env' in + (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent) + end + type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = @@ -365,7 +381,8 @@ let inInductive : inductive_obj -> obj = open_function = open_inductive; classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; - discharge_function = discharge_inductive } + discharge_function = discharge_inductive; + rebuild_function = infer_inductive_subtyping } let declare_projections mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in diff --git a/library/declare.mli b/library/declare.mli index f70d594d7e..6a09434645 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/declaremods.ml b/library/declaremods.ml index c98d4a7f31..e7aa5bd0d6 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -589,7 +589,6 @@ 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 (); if_xml (Hook.get f_xml_start_module) mp; mp @@ -629,7 +628,6 @@ let end_module () = assert (eq_full_path (fst newoname) (fst oldoname)); 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 @@ -701,7 +699,6 @@ 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 (); if_xml (Hook.get f_xml_start_module_type) mp; mp @@ -719,7 +716,6 @@ let end_modtype () = assert (eq_full_path (fst oname) (fst oldoname)); 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 @@ -894,8 +890,7 @@ let get_library_native_symbols dir = let start_library dir = let mp = Global.start_library dir in openmod_info := default_module_info; - Lib.start_compilation dir mp; - Lib.add_frozen_state () + Lib.start_compilation dir mp let end_library_hook = ref ignore let append_end_library_hook f = diff --git a/library/declaremods.mli b/library/declaremods.mli index 3917fe8d64..1f2aaf7b54 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/decls.ml b/library/decls.ml index 2952c258a5..973fe144dd 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/decls.mli b/library/decls.mli index 1ca7f89469..478f0bca0d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 cea1fd7d6e..1673e13cca 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 ea4a9424e5..69bb6744e5 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 1ba86699d3..5b17855dce 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -122,12 +122,22 @@ let lookup_modtype kn = lookup_modtype kn (env()) let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body cb = Declareops.body_of_constant (opaque_tables ()) cb + +let instantiate cb c = + let open Declarations in + match cb.const_universes with + | Monomorphic_const _ -> c, Univ.AUContext.empty + | Polymorphic_const ctx -> c, ctx + +let body_of_constant_body cb = + let open Declarations in + let otab = opaque_tables () in + match cb.const_body with + | Undef _ -> None + | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) + | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) + let body_of_constant cst = body_of_constant_body (lookup_constant cst) -let constraints_of_constant_body cb = - Declareops.constraints_of_constant (opaque_tables ()) cb -let universes_of_constant_body cb = - Declareops.universes_of_constant (opaque_tables ()) cb (** Operations on kernel names *) @@ -163,69 +173,60 @@ open Globnames (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -let type_of_global_unsafe r = - let env = env() in +let constr_of_global_in_context env r = + let open Constr in match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in - Vars.subst_instance_constr (Univ.UContext.instance univs) ty + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + mkConstU (c, Univ.make_abstract_instance univs), univs | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = - if mib.Declarations.mind_polymorphic then - Univ.UContext.instance mib.Declarations.mind_universes - else Univ.Instance.empty - in - Inductive.type_of_inductive env (specif, inst) + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + mkIndU (ind, Univ.make_abstract_instance univs), univs | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Univ.UContext.instance mib.Declarations.mind_universes in - Inductive.type_of_constructor (cstr,inst) specif + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + mkConstructU (cstr, Univ.make_abstract_instance univs), univs let type_of_global_in_context env r = - let open Declarations in match r with - | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty | ConstRef c -> - let cb = Environ.lookup_constant c env in - let univs = - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb in - Typeops.type_of_constant_type env cb.Declarations.const_type, univs + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in + Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let univs = - 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 + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in + Inductive.type_of_inductive env (specif, inst), 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 Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty - in - let inst = Univ.UContext.instance univs in - Inductive.type_of_constructor (cstr,inst) specif, univs + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + let inst = Univ.make_abstract_instance univs in + Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = - let open Declarations in match r with - | VarRef id -> Univ.UContext.empty + | VarRef id -> Univ.AUContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - Declareops.universes_of_polymorphic_constant - (Environ.opaque_tables env) cb + Declareops.constant_polymorphic_context cb | IndRef ind -> let (mib, oib) = Inductive.lookup_mind_specif env ind in - Univ.instantiate_univ_context mib.mind_universes + Declareops.inductive_polymorphic_context mib | ConstructRef cstr -> - let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Univ.instantiate_univ_context mib.mind_universes + let (mib,oib) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Declareops.inductive_polymorphic_context mib let universes_of_global gr = universes_of_global (env ()) gr diff --git a/library/global.mli b/library/global.mli index a4a38ce846..48bcfa989f 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -89,12 +89,15 @@ val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> Term.constr option -val body_of_constant_body : Declarations.constant_body -> Term.constr option -val constraints_of_constant_body : - Declarations.constant_body -> Univ.constraints -val universes_of_constant_body : - Declarations.constant_body -> Univ.universe_context + +val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) + +val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option +(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** Global universe name <-> level mapping *) type universe_names = @@ -126,26 +129,22 @@ val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool -val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types Univ.in_universe_context -(** Returns the type of the constant in its global or local universe +val constr_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) -val type_of_global_unsafe : Globnames.global_reference -> Constr.types -(** Returns the type of the constant, forgetting its universe context if - it is polymorphic, use with care: for polymorphic constants, the - type cannot be used to produce a term used by the kernel. For safe - handling of polymorphic global references, one should look at a - particular instantiation of the reference, in some particular - universe context (part of an [env] or [evar_map]), see - e.g. [type_of_constant_in]. If you want to create a fresh instance - of the reference and get its type look at [Evd.fresh_global] or - [Evarutil.new_global] and [Retyping.get_type_of]. *) +val type_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.universe_context +val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 9aeb379737..dc9541a0d5 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/globnames.mli b/library/globnames.mli index f4956e3df2..0b5971b6e1 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 a305214e82..fe014ef68e 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/goptions.mli b/library/goptions.mli index f612c4e369..3100c1ce72 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 6aee63c744..c12fa94791 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -128,11 +128,11 @@ let compute_head = function let is_Def = function Declarations.Def _ -> true | _ -> false in let body = if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body - then Declareops.body_of_constant (Environ.opaque_tables env) cb else None + then Global.body_of_constant cst else None in (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) + | Some (c, _) -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> diff --git a/library/heads.mli b/library/heads.mli index 5acf5f54f7..1ce66c841e 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 8f3bfc17e4..b7125fc85d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -431,12 +431,13 @@ 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 *) - Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) + let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = Global.type_of_global_unsafe (IndRef ind) in + let ar, _ = Global.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) @@ -674,7 +675,7 @@ let projection_implicits env p impls = let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in - let t = Global.type_of_global_unsafe ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in let enriching = Option.default flags.auto enriching in let isrigid,autoimpls = compute_auto_implicits env flags enriching t in let l' = match l with diff --git a/library/impargs.mli b/library/impargs.mli index 3919a519c9..4b78f54eac 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 c9e325ee57..be53aabaa4 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 6abac4de44..6fe9efc6ec 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 623d2537aa..882f620862 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 3e95eaa7d9..77979c9159 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 9d71a854f0..a24d20c681 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,7 +27,6 @@ type node = | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_entry = object_name * node @@ -80,7 +79,6 @@ let classify_segment seg = | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" (str "there are still opened " ++ str (module_kind ty) ++ str "s") - | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -254,10 +252,6 @@ let add_anonymous_leaf ?(cache_first = true) obj = cache_object (oname,obj) end -let add_frozen_state () = - add_anonymous_entry - (FrozenState (Summary.freeze_summaries ~marshallable:`No)) - (* Modules. *) let is_opening_node = function @@ -408,7 +402,7 @@ let find_opening_node id = type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t @@ -471,9 +465,10 @@ let add_section_replacement f g poly hyps = 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 + let inst = Univ.UContext.instance ctx in + let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + sectab := (vars,f (inst,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = @@ -544,7 +539,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | FrozenState _ -> None | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -585,8 +579,7 @@ let freeze ~marshallable = | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection []) - | _, FrozenState _ -> None) + | n, ClosedSection _ -> Some (n,ClosedSection [])) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -596,8 +589,7 @@ let unfreeze st = lib_state := st let init () = unfreeze initial_lib_state; - Summary.init_summaries (); - add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) + Summary.init_summaries () (* Misc *) @@ -653,3 +645,16 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) + +let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = + let open Univ in + let len = LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (AUContext.size auctx - 1) subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 9f9d8c7e5f..f1c9bfca24 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -23,7 +23,6 @@ type node = | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -61,8 +60,6 @@ val pull_to_head : Libnames.object_name -> unit for each of them *) val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name -val add_frozen_state : unit -> unit - (** {6 ... } *) (** The function [contents] gives access to the current entire segment *) @@ -123,8 +120,6 @@ val end_modtype : Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment -(** [Lib.add_frozen_state] must be called after each of the above functions *) - (** {6 Compilation units } *) val start_compilation : Names.DirPath.t -> Names.module_path -> unit @@ -162,7 +157,7 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t +type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t @@ -188,3 +183,5 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/libnames.ml b/library/libnames.ml index 50f28b0205..0453f15e87 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 57013ef82e..b6d6f7f3bc 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 897591762c..013c6fa0a5 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/libobject.mli b/library/libobject.mli index 51b9af059f..1a21ece2b4 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 5a5f99cc51..20ecc2c229 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -575,7 +575,7 @@ let require_library_from_dirpath modrefl export = 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 b9044b60dd..604167804d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/library.mllib b/library/library.mllib index 6f433b77d1..d94fc22919 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,3 +1,4 @@ +Univops Nameops Libnames Globnames diff --git a/library/loadpath.ml b/library/loadpath.ml index ad429ea840..757e972b1a 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/loadpath.mli b/library/loadpath.mli index 4e79edbdcf..26ed30674a 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 0b5dfd8d0e..adfe6f5a5d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 abfc09db8d..88290f4850 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 93e9c03cee..68fdbb4f38 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/nametab.mli b/library/nametab.mli index 095ac4f9df..be57f5dcc6 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 95bd819d66..03e4610a6d 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 12c71c9991..780a4e8dc8 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 c7bf95fd41..69eff830da 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/summary.mli b/library/summary.mli index 1b57613cb7..a6ad49950e 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-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/library/univops.ml b/library/univops.ml new file mode 100644 index 0000000000..3bafb824d1 --- /dev/null +++ b/library/univops.ml @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Univ + +let universes_of_constr c = + let rec aux s c = + match kind_of_term c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/library/univops.mli b/library/univops.mli new file mode 100644 index 0000000000..09147cb41c --- /dev/null +++ b/library/univops.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Term +open Univ + +(** Shrink a universe context to a restricted set of variables *) + +val universes_of_constr : constr -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set |