From 731a842cb5af9631349a549090ea3eb6b1d386b2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 5 Mar 2011 16:41:46 +0000
Subject: Fixing injection bug #2493 (regression introduced by fixing injection
 bug #2255 from 8.2pl2: use of unification might support cumulativity).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13873 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index a2e76cd9e3..079a18c1ef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -881,8 +881,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = type_of env sigma w in
-            if Evarconv.e_conv env evdref w_type a then
-              applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+            if Evarconv.e_cumul env evdref w_type a then
+              applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
 	| None -> anomaly "Not enough components to build the dependent tuple"
-- 
cgit v1.2.3