From 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 5 Sep 2014 20:27:37 +0200 Subject: Fix checker treatment of inductives using subst_instances instead of subst_univs_levels. --- checker/environ.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'checker/environ.ml') 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) -- cgit v1.2.3