From 5bf063c15468bb81f0f48b583f600250cd829aee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:37:46 +0200
Subject: UnivGen.constr_of_glob_univ -> Constr.mkRef

---
 tactics/equality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3e3ef78c5d..c4a6b1605d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1792,7 +1792,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
       try
         let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
         let u = EInstance.kind sigma u in
-        let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+        let eq = Constr.mkRef (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
         | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
@@ -1843,7 +1843,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     try
       let lbeq,u,(_,x,y) = find_eq_data_decompose c in
       let u = EInstance.kind sigma u in
-      let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in
+      let eq = Constr.mkRef (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
       if EConstr.eq_constr sigma x y then failwith "caught";
-- 
cgit v1.2.3