From 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 5 Aug 2008 15:38:31 +0000
Subject: Correction de bugs: - evarconv: mauvaise idée d'utiliser la
 conversion sur la tête d'un   terme applicatif au moment de tester f u1 .. un
 = g v1 .. vn au   premier ordre : on revient sur l'algo tel qu'il était avant
 le   commit 11187. - Bug #1887 (format récursif cassé à cause de la
 vérification des idents). - Nouveau choix de formattage du message "Tactic
 Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage.

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

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4d57108603..667ea458cc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -273,11 +273,10 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f1 i =
-	  if l1 <> [] && l2 <> [] then
-            ise_list2 i (fun i -> evar_conv_x env i CONV)
-	      (flex1::l1) (flex2::l2)
+	  if flex1 = flex2 then
+	    ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
 	  else
-	    (i,false)
+	     (i,false)
 	and f2 i =
 	  (try conv_record env i
              (try check_conv_record appr1 appr2
-- 
cgit v1.2.3