From 9b9ed1245225fc95374b070f5f5ed699337448fc Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 7 Jun 2002 17:18:52 +0000
Subject: L'ordre supérieur avait quelque peu été oublié dans l'unification...
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2772 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 049659b89..772eae76b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -173,6 +173,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f2 () =
           (flex1 = flex2)
+	  & (List.length l1 = List.length l2)
 	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 	and f3 () =
 	  (try conv_record env isevars 
-- 
cgit v1.2.3