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


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


From 7320cd84f92793572550d1fe1a2181f40466fa81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2020 17:50:40 +0200
Subject: Similarly remove the explicit graph argument in the ~evar conversion
 API.

---
 pretyping/reductionops.ml | 6 ++++--
 pretyping/typing.ml       | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index db2f5c6209..3352bfce38 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1094,7 +1094,8 @@ let f_conv_leq ?l2r ?reds env ?evars x y =
 let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
-    let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
+    let env = Environ.set_universes (Evd.universes sigma) env in
+    let _ = f ~reds env ~evars x y in
     true
   with Reduction.NotConvertible -> false
     | e ->
@@ -1112,7 +1113,8 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y =
     | Reduction.CONV -> f_conv
     | Reduction.CUMUL -> f_conv_leq
   in
-    try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true
+    let env = Environ.set_universes (Evd.universes sigma) env in
+    try f ~reds:ts env ~evars:(safe_evar_value sigma) x y; true
     with Reduction.NotConvertible -> false
     | Univ.UniverseInconsistency _ -> false
     | e ->
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 756ccd3438..e40dea06e7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -296,7 +296,8 @@ let judge_of_letin env name defj typj j =
     uj_type = subst1 defj.uj_val j.uj_type }
 
 let check_hyps_inclusion env sigma x hyps =
-  let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+  let env = Environ.set_universes (Evd.universes sigma) env in
+  let evars = Evarutil.safe_evar_value sigma in
   Typeops.check_hyps_inclusion env ~evars x hyps
 
 let type_of_constant env sigma (c,u) =
-- 
cgit v1.2.3