diff options
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index a04e95cfc..710ebc712 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -108,10 +108,9 @@ type const_evaluation_result = NoBody | Opaque (* Constant types *) -let universes_and_subst_of cb u = +let constraints_of cb u = let univs = cb.const_universes in - let subst = Univ.make_universe_subst u univs in - subst, Univ.instantiate_univ_context subst univs + Univ.subst_instance_constraints u (Univ.UContext.constraints univs) let map_regular_arity f = function | RegularArity a as ar -> @@ -123,8 +122,8 @@ let map_regular_arity f = function let constant_type env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then - let subst, csts = universes_and_subst_of cb u in - (map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts) + let csts = constraints_of cb u in + (map_regular_arity (subst_instance_constr u) cb.const_type, csts) else cb.const_type, Univ.Constraint.empty exception NotEvaluableConst of const_evaluation_result @@ -135,8 +134,7 @@ let constant_value env (kn,u) = | Def l_body -> let b = force_constr l_body in if cb.const_polymorphic then - let subst = Univ.make_universe_subst u cb.const_universes in - subst_univs_level_constr subst b + subst_instance_constr u (force_constr l_body) else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) |