diff options
Diffstat (limited to 'library')
44 files changed, 131 insertions, 147 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 db3dbcbd92..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 *) @@ -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; 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 187b749b87..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 *) 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 6d80012f47..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,54 +173,53 @@ 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 = Declareops.inductive_polymorphic_instance mib 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 = Declareops.inductive_polymorphic_instance mib 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 = 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 = Declareops.inductive_polymorphic_context mib 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 = Declareops.inductive_polymorphic_context mib in - let inst = Univ.UContext.instance univs in + let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = 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 Declareops.inductive_polymorphic_context mib 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 8127316d73..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 *) @@ -465,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 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.AUContext.instance ctx,args) exps, + sectab := (vars,f (inst,args) exps, g (sechyps,subst,ctx) abs)::sl let add_section_kn poly kn = @@ -644,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 284d339801..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 *) @@ -183,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 db05ad2b7b..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 *) 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/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 index 60c12f0d81..3bafb824d1 100644 --- a/library/univops.ml +++ b/library/univops.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 *) @@ -8,7 +8,6 @@ open Term open Univ -open Declarations let universes_of_constr c = let rec aux s c = @@ -21,44 +20,6 @@ let universes_of_constr c = | _ -> fold_constr aux s c in aux LSet.empty c -let universes_of_inductive mind = - let process auctx = - let u = Univ.AUContext.instance auctx in - let univ_of_one_ind oind = - let arity_univs = - Context.Rel.fold_outside - (fun decl unvs -> - Univ.LSet.union - (Context.Rel.Declaration.fold_constr - (fun cnstr unvs -> - let cnstr = Vars.subst_instance_constr u cnstr in - Univ.LSet.union - (universes_of_constr cnstr) unvs) - decl Univ.LSet.empty) unvs) - oind.mind_arity_ctxt ~init:Univ.LSet.empty - in - Array.fold_left (fun unvs cns -> - let cns = Vars.subst_instance_constr u cns in - Univ.LSet.union (universes_of_constr cns) unvs) arity_univs - oind.mind_nf_lc - in - let univs = - Array.fold_left - (fun unvs pk -> - Univ.LSet.union - (univ_of_one_ind pk) unvs - ) - Univ.LSet.empty mind.mind_packets - in - let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context auctx) in - let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in - univs - in - match mind.mind_universes with - | Monomorphic_ind _ -> LSet.empty - | Polymorphic_ind auctx -> process auctx - | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) - 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. *) diff --git a/library/univops.mli b/library/univops.mli index 5b499c75bc..09147cb41c 100644 --- a/library/univops.mli +++ b/library/univops.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 *) @@ -8,10 +8,8 @@ open Term open Univ -open Declarations (** Shrink a universe context to a restricted set of variables *) val universes_of_constr : constr -> universe_set -val universes_of_inductive : mutual_inductive_body -> universe_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set |