From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 13:57:10 +0100 Subject: Returning instance instead of substitution in universe context abstraction. This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1. --- kernel/mod_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f7e755f00..b7eb481ee 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let ctx = Univ.ContextSet.of_context ctx in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx | Polymorphic_const uctx -> - let subst, ctx = Univ.abstract_universes ctx in - let c = Vars.subst_univs_level_constr subst c in + let inst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let () = if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then error_incorrect_with_constraint lab -- cgit v1.2.3