From 790243ed041f0626cd2d1613473b8f393ecccd56 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Jul 2001 08:47:30 +0000
Subject: la conversion ne doit être testé dans evar_conv qu'en absence de evar

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6783e70a4f..f40ad4dc00 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -56,15 +56,16 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   let term1 = whd_castappevar sigma term1 in
   let term2 = whd_castappevar sigma term2 in
 (*
- if eq_constr term1 term2 then 
+  if eq_constr term1 term2 then 
     true
-  else if (not(has_undefined_isevars isevars term1)) &
-    not(has_undefined_isevars isevars term2) 
-  then 
-    is_fconv pbty env (evars_of isevars) term1 term2
-  else
+  else 
 *)
-  (is_fconv pbty env sigma term1 term2) or
+  (* Maybe convertible but since reducing can erase evars which [evar_apprec]*)
+  (* could have found, we do it only if the terms are free of evar  *)
+  (not (has_undefined_isevars isevars term1) &
+   not (has_undefined_isevars isevars term2) &
+   is_fconv pbty env (evars_of isevars) term1 term2) 
+  or
   if ise_undefined isevars term1 then
     solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2)
   else if ise_undefined isevars term2 then
-- 
cgit v1.2.3