From 1d01533266b247cbc32903935963674acf7c6c54 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 1 Oct 2015 16:05:48 +0200
Subject: Univs: forgot a substitution in mod_typing.

---
 kernel/mod_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 3be89afbd..922652287 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -111,6 +111,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
 	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = Vars.subst_instance_constr cus typ in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
-- 
cgit v1.2.3