From 9963243587e1e2af7737c85012200be84d645dad Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 21 Nov 2008 12:57:44 +0000
Subject: fixed exponential behavior of evar unif (ground case)

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c682829087..efbe2f3358 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -164,10 +164,9 @@ let rec evar_conv_x env evd pbty term1 term2 =
   (* 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.
      Note: incomplete heuristic... *)
-  if is_ground_term evd term1 && is_ground_term evd term2 &
-     is_fconv pbty env (evars_of evd) term1 term2
+  if is_ground_term evd term1 && is_ground_term evd term2
   then
-    (evd,true)
+    (evd,is_fconv pbty env (evars_of evd) term1 term2)
   else
   let term1 = apprec_nohdbeta env evd term1 in
   let term2 = apprec_nohdbeta env evd term2 in
-- 
cgit v1.2.3