Applying Enrico Tassi's patch for giving priority to delta over eta in

unification (evarconv.ml). Works better for compiling
math. comp. library while seems ok on other examples.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14153 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b3b9ec393..196adaae5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -357,25 +357,6 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	     let c = nf_evar i c1 in
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
-    (* Eta-expansion *)
-    | Rigid c1, _ when isLambda c1 ->
-	assert (l1 = []);
-	let (na,c1,c'1) = destLambda c1 in
-        let c = nf_evar evd c1 in
-	let env' = push_rel (na,None,c) env in
-        let appr1 = evar_apprec env' evd [] c'1 in
-	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
-	evar_eqappr_x ts env' evd CONV appr1 appr2
-
-    | _, Rigid c2 when isLambda c2 ->
-	assert (l2 = []);
-	let (na,c2,c'2) = destLambda c2 in
-        let c = nf_evar evd c2 in
-	let env' = push_rel (na,None,c) env in
-	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
-        let appr2 = evar_apprec env' evd [] c'2 in
-	evar_eqappr_x ts env' evd CONV appr1 appr2
-
     | Flexible ev1, (Rigid _ | PseudoRigid _) ->
 	if
 	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
@@ -432,6 +413,25 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in
 	ise_try evd [f3; f4]
 
+    (* Eta-expansion *)
+    | Rigid c1, _ when isLambda c1 ->
+	assert (l1 = []);
+	let (na,c1,c'1) = destLambda c1 in
+        let c = nf_evar evd c1 in
+	let env' = push_rel (na,None,c) env in
+        let appr1 = evar_apprec env' evd [] c'1 in
+	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
+	evar_eqappr_x ts env' evd CONV appr1 appr2
+
+    | _, Rigid c2 when isLambda c2 ->
+	assert (l2 = []);
+	let (na,c2,c'2) = destLambda c2 in
+        let c = nf_evar evd c2 in
+	let env' = push_rel (na,None,c) env in
+	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
+        let appr2 = evar_apprec env' evd [] c'2 in
+	evar_eqappr_x ts env' evd CONV appr1 appr2
+
     | Rigid c1, Rigid c2 -> begin
         match kind_of_term c1, kind_of_term c2 with