From f34dcb97406611704c93970ea623d6a8587e5ba8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:43:23 +0200
Subject: Moving the remaining Refiner functions to Tacmach.

---
 plugins/ssr/ssrcommon.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5c25db1a82..5f463f8de4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -748,7 +748,7 @@ let pf_abs_cterm gl n c0 = abs_cterm (pf_env gl) (project gl) n c0
 (* }}} *)
 
 let pf_merge_uc uc gl =
-  re_sig (sig_it gl) (Evd.merge_universe_context (Refiner.project gl) uc)
+  re_sig (sig_it gl) (Evd.merge_universe_context gl.Evd.sigma uc)
 let pf_merge_uc_of sigma gl =
   let ucst = Evd.evar_universe_context sigma in
   pf_merge_uc ucst gl
-- 
cgit v1.2.3