From 5378c756b3aa114c4def0ec116a0654eea7bf95f Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 18 Feb 2002 17:30:51 +0000
Subject: bug #134: on appelait solve_simple_eqn avec une evar qui etait
 resolue par comparaison de ses arguments

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6269dc9413..e9a1b03bac 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -83,6 +83,7 @@ let check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
+
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
@@ -143,8 +144,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
           (* First compare extra args for better failure message *)
           list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 &
-	  solve_simple_eqn evar_conv_x env isevars
-	    (pbty,ev1,applist(term2,deb2))
+	  evar_conv_x env isevars pbty term1 (applist(term2,deb2))
 	and f4 () =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
@@ -160,8 +160,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
           (* First compare extra args for better failure message *)
           list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 &
-	  solve_simple_eqn evar_conv_x env isevars
-            (pbty,ev2,applist(term1,deb1))
+	  evar_conv_x env isevars pbty (applist(term1,deb1)) term2
 	and f4 () =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
-- 
cgit v1.2.3