From 9a026fcaeb3fa2678b9c93da8204f9f1ddcc0b31 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Sep 2020 09:54:42 +0200
Subject: Remove the compare_graph field from the conversion API.

We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.
---
 pretyping/reductionops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 08a6db5639..bea62c8bef 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1138,8 +1138,7 @@ let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
 
 let sigma_univ_state =
   let open Reduction in
-  { compare_graph = Evd.universes;
-    compare_sorts = sigma_compare_sorts;
+  { compare_sorts = sigma_compare_sorts;
     compare_instances = sigma_compare_instances;
     compare_cumul_instances = sigma_check_inductive_instances; }
 
@@ -1164,9 +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 sigma' =
           conv_fun pb ~l2r:false sigma ts
-            env (sigma, sigma_univ_state) x y in
+            env graph (sigma, sigma_univ_state) x y in
         Some sigma'
   with
   | Reduction.NotConvertible -> None
-- 
cgit v1.2.3