From b335fccae5514ef738376354aa619e08bb221d5c Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Sat, 6 Jul 2019 21:17:20 +0200
Subject: Solve universe error with SSR 'rewrite !term'

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

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 220b9bc475..1f125a3c59 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -255,7 +255,9 @@ let tclNOTSAMEGOAL tac =
     Proofview.Goal.goals >>= fun gls ->
     let check accu gl' =
       gl' >>= fun gl' ->
-      let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in
+      let accu = accu || Proofview.Progress.goal_equal
+                            ~evd:sigma ~extended_evd:(project gl') ev (goal gl')
+      in
       Proofview.tclUNIT accu
     in
     Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
-- 
cgit v1.2.3