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.

---
 kernel/reduction.ml                | 6 +++---
 kernel/reduction.mli               | 2 +-
 kernel/typeops.mli                 | 2 +-
 plugins/ssrmatching/ssrmatching.ml | 3 ++-
 pretyping/reductionops.ml          | 6 ++++--
 pretyping/typing.ml                | 3 ++-
 6 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8258c1c086..96bf370342 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -189,7 +189,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
-  ?evars:((existential->constr option) * UGraph.t) ->
+  ?evars:(existential->constr option) ->
   'a -> 'a -> unit
 
 exception NotConvertible
@@ -888,8 +888,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
         ()
 
 (* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
-  let evars, univs = evars in
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
+  let univs = Environ.universes env in
   if Flags.profile then
     let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
       CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3c747f0ff8..7d32596f74 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,7 +31,7 @@ exception NotConvertible
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 type 'a extended_conversion_function =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
-  ?evars:((existential->constr option) * UGraph.t) ->
+  ?evars:(existential->constr option) ->
   'a -> 'a -> unit
 
 type conv_pb = CONV | CUMUL
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 87a5666fcc..d381e55dd6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+val check_hyps_inclusion : env -> ?evars:(existential->constr option) ->
   GlobRef.t -> Constr.named_context -> unit
 
 (** Types for primitives *)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5dedae6388..cdd15acb0d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -204,7 +204,8 @@ exception NoProgress
 (*      comparison can be much faster than the HO one.          *)
 
 let unif_EQ env sigma p c =
-  let evars = existential_opt_value0 sigma, Evd.universes sigma in
+  let env = Environ.set_universes (Evd.universes sigma) env in
+  let evars = existential_opt_value0 sigma in
   try let _ = Reduction.conv env p ~evars c in true with _ -> false
 
 let unif_EQ_args env sigma pa a =
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