diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
| commit | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (patch) | |
| tree | d67a1ead218ca15becb33b605426cb5429323b60 /checker/environ.ml | |
| parent | 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 (diff) | |
Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
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) |