From f96dc97f48df5d0fdf252be5f28478a58be77961 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Wed, 17 Sep 2014 20:51:40 +0200
Subject: Fix bug #3593, making constr_eq and progress work up to equality of
 universes, along with a few other functions in evd.

---
 proofs/goal.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/goal.ml')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 55de87261..dea704a68 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -94,7 +94,7 @@ let solution sigma g =
 let equal evars1 gl1 evars2 gl2 =
   let evi1 = content evars1 gl1 in
   let evi2 = content evars2 gl2 in
-  Evd.eq_evar_info evi1 evi2
+  Evd.eq_evar_info evars2 evi1 evi2
 
 (* [contained_in_info e evi] checks whether the evar [e] appears in
    the hypotheses, the conclusion or the body of the evar_info
-- 
cgit v1.2.3