From fe0bf68ccfe9ab635012b8e396011d20e8c25612 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 23 Jan 2003 17:30:03 +0000
Subject: reparation des contribs: lors de l'unification, reduire les beta
 redexes avant d'expanser les constantes

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 289a80ced8..623d0e99d5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -218,7 +218,14 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	      with Not_found -> check_conv_record appr2 appr1)
            with _ -> false)
 	and f4 () =
-	  match eval_flexible_term env flex2 with
+          (* heuristic: unfold second argument first, exception made
+             if the first argument is a beta-redex (expand a constant
+             only if necessary) *)
+          let val2 =
+            match kind_of_term flex1 with
+                Lambda _ -> None
+              | _ -> eval_flexible_term env flex2 in
+	  match val2 with
 	    | Some v2 ->
 		evar_eqappr_x env isevars pbty
 		  appr1 (evar_apprec env isevars l2 v2)
-- 
cgit v1.2.3