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.

---
 plugins/ssrmatching/ssrmatching.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

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 =
-- 
cgit v1.2.3