diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |