From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- kernel/mod_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 4fc777c4..ff44f0f5 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -104,7 +104,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let csti = Univ.enforce_eq_instances cus newus cst in let csta = Univ.Constraint.union csti ccst in let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (Univ.check_constraints cst (Environ.universes env')) then + let () = if not (UGraph.check_constraints cst (Environ.universes env')) then error_incorrect_with_constraint lab in let cst = match cb.const_body with -- cgit v1.2.3