From eb5a67de1fc586acc588d5c61c84df670284f054 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2020 17:40:01 +0200
Subject: Pick the universe graph out of the environment in conversion API.

---
 kernel/subtyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 28baa82666..76a1c190be 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -85,7 +85,7 @@ let make_labmap mp list =
 
 let check_conv_error error why cst poly f env a1 a2 =
   try
-    let cst' = f env (Environ.universes env) a1 a2 in
+    let cst' = f env a1 a2 in
       if poly then
         if Constraint.is_empty cst' then cst
         else error (IncompatiblePolymorphism (env, a1, a2))
-- 
cgit v1.2.3