diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 39 |
1 files changed, 12 insertions, 27 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3b7e3ae544..f09f782008 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -405,19 +405,12 @@ let add_constant_key kn cb linkinfo env = let add_constant kn cb env = add_constant_key kn cb no_link_info env -let constraints_of cb u = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Constraint.empty - | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty - | Polymorphic_const _ctx -> - let csts = constraints_of cb u in - (subst_instance_constr u cb.const_type, csts) + let uctx = Declareops.constant_polymorphic_context cb in + let csts = Univ.AUContext.instantiate u uctx in + (subst_instance_constr u cb.const_type, csts) type const_evaluation_result = NoBody | Opaque @@ -425,20 +418,14 @@ exception NotEvaluableConst of const_evaluation_result let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in - if Declareops.constant_is_polymorphic cb then - let cst = constraints_of cb u in - let b' = match cb.const_body with - | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) - | OpaqueDef _ -> None - | Undef _ -> None - in - b', subst_instance_constr u cb.const_type, cst - else - let b' = match cb.const_body with - | Def l_body -> Some (Mod_subst.force_constr l_body) - | OpaqueDef _ -> None - | Undef _ -> None - in b', cb.const_type, Univ.Constraint.empty + let uctx = Declareops.constant_polymorphic_context cb in + let cst = Univ.AUContext.instantiate u uctx in + let b' = match cb.const_body with + | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) + | OpaqueDef _ -> None + | Undef _ -> None + in + b', subst_instance_constr u cb.const_type, cst (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant @@ -447,9 +434,7 @@ let constant_value_and_type env (kn, u) = (* constant_type gives the type of a constant *) let constant_type_in env (kn,u) = let cb = lookup_constant kn env in - if Declareops.constant_is_polymorphic cb then - subst_instance_constr u cb.const_type - else cb.const_type + subst_instance_constr u cb.const_type let constant_value_in env (kn,u) = let cb = lookup_constant kn env in |