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.

---
 pretyping/reductionops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bea62c8bef..db2f5c6209 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1163,10 +1163,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
       | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
-        let graph = Evd.universes sigma in
+        let env = Environ.set_universes (Evd.universes sigma) env in
         let sigma' =
           conv_fun pb ~l2r:false sigma ts
-            env graph (sigma, sigma_univ_state) x y in
+            env (sigma, sigma_univ_state) x y in
         Some sigma'
   with
   | Reduction.NotConvertible -> None
-- 
cgit v1.2.3