From 612ea3d4b3c7d7e00616b009050803cd7b7f763e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Jan 2007 17:36:04 +0000
Subject: Correction d'un bug d'unification-pattern dans l'algo d'unification
 des tactiques (ne marchait que si l'instance était une application).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9516 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml         | 15 +++++++--------
 test-suite/success/unification.v |  6 ++++++
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7843b2226e..a70f0876b8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -147,16 +147,15 @@ let unify_0 env sigma cv_pb mod_delta m n =
 	| LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN
 	| _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c)
 	    
-	| App (f1,l1), App (f2,l2) ->
-	    if
-	      isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN)
-	    then
+	| App (f1,l1), _ when
+	    isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) ->
 	      solve_pattern_eqn_array curenv f1 l1 cN substn
-	    else if
-		isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM)
-	    then
+
+	| _, App (f2,l2) when
+	    isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) ->
 	      solve_pattern_eqn_array curenv f2 l2 cM substn
-	    else
+
+	| App (f1,l1), App (f2,l2) ->
 	      let len1 = Array.length l1
 	      and len2 = Array.length l2 in
               let (f1,l1,f2,l2) =
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 7acbb7d05e..2d6dabf264 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -15,6 +15,12 @@ Proof.
 intros; apply (H _ H0).
 Qed.
 
+Lemma l3 : (forall P, ~(exists x:nat, P x))
+         -> forall P:nat->Prop, ~(exists x:nat, P x -> P x).
+Proof.
+intros; apply H.
+Qed.
+
 
 (* Example submitted for Zenon *)
 
-- 
cgit v1.2.3