diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declareops.ml | 28 | ||||
| -rw-r--r-- | kernel/declareops.mli | 9 | ||||
| -rw-r--r-- | kernel/environ.ml | 10 | ||||
| -rw-r--r-- | kernel/environ.mli | 5 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 4 |
5 files changed, 12 insertions, 44 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1337036b8b..cf6d3c55e1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -67,24 +67,14 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let universes_of_polymorphic_constant otab cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx - let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true -let constant_polymorphic_instance cb = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.AUContext.instance ctx - let constant_polymorphic_context cb = match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true @@ -268,19 +258,11 @@ let subst_mind_body sub mib = mind_typing_flags = mib.mind_typing_flags; } -let inductive_polymorphic_instance mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind ctx -> Univ.AUContext.instance ctx - | Cumulative_ind cumi -> - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) - let inductive_polymorphic_context mib = match mib.mind_universes with - | Monomorphic_ind _ -> Univ.UContext.empty - | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + | Monomorphic_ind _ -> Univ.AUContext.empty + | Polymorphic_ind ctx -> ctx + | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi let inductive_is_polymorphic mib = match mib.mind_universes with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 7350724b8b..987c1adaf1 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,8 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool -val constant_polymorphic_instance : constant_body -> universe_instance -val constant_polymorphic_context : constant_body -> universe_context +val constant_polymorphic_context : constant_body -> abstract_universe_context (** Is the constant polymorphic? *) val constant_is_polymorphic : constant_body -> bool @@ -43,9 +42,6 @@ val type_of_constant : constant_body -> constant_type (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) -val universes_of_polymorphic_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.universe_context - val is_opaque : constant_body -> bool (** Side effects *) @@ -68,8 +64,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance -val inductive_polymorphic_context : mutual_inductive_body -> universe_context +val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context (** Is the inductive polymorphic? *) val inductive_is_polymorphic : mutual_inductive_body -> bool diff --git a/kernel/environ.ml b/kernel/environ.ml index ca2c8e1356..b01b652001 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -247,17 +247,11 @@ let constant_type env (kn,u) = let csts = constraints_of cb u in (map_regular_arity (subst_instance_constr u) cb.const_type, csts) -let constant_instance env kn = - let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> Univ.Instance.empty - | Polymorphic_const ctx -> Univ.AUContext.instance ctx - let constant_context env kn = let cb = lookup_constant kn env in match cb.const_universes with - | Monomorphic_const _ -> Univ.UContext.empty - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx type const_evaluation_result = NoBody | Opaque | IsProj diff --git a/kernel/environ.mli b/kernel/environ.mli index f8887d8e83..cd7a9d2791 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -160,10 +160,7 @@ val constant_value_and_type : env -> constant puniverses -> constr option * constant_type * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.universe_context -(** The universe isntance associated to the constant, empty if not - polymorphic *) -val constant_instance : env -> constant -> Univ.universe_instance +val constant_context : env -> constant -> Univ.abstract_universe_context (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9d72622068..da7fcd6f23 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1959,14 +1959,14 @@ let param_name = Name (id_of_string "params") let arg_name = Name (id_of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_polymorphic_instance mb in + let u = Declareops.inductive_polymorphic_context mb in let f i stack ob = let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in let j = push_symbol (SymbInd (mind,i)) in let name = Gind ("", (mind, i)) in let accu = let args = - if Univ.Instance.is_empty u then + if Int.equal (Univ.AUContext.size u) 0 then [|get_ind_code j; MLarray [||]|] else [|get_ind_code j|] in |