Raffinement de l'heuristique d'unification dans sig_clausale_forme

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

1 files changed, 17 insertions, 9 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 338addc4df..fdd02fe92e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -638,15 +638,23 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
       let headpat = nf_betadeltaiota env sigma ty in
       let nf_ty = nf_betadeltaiota env sigma dFLTty in
       let bindings =
-	list_try_find
-	  (fun ty -> 
-             try 
-            (* Test inutile car somatch ne prend pas en compte les univers *) 
-	       if is_Type headpat & is_Type ty then
-		 []
-	       else
-		 matches (pattern_of_constr headpat) ty 
-             with PatternMatchingFailure -> failwith "caught")
+        (* Test inutile car somatch ne prend pas en compte les univers *) 
+	if is_Type headpat & is_Type nf_ty then
+	  []
+        else
+          let headpat = pattern_of_constr headpat in
+          let weakpat = pattern_of_constr (nf_betaiota ty) in
+	  list_try_find
+	    (fun ty -> 
+              try 
+		matches headpat ty 
+              with PatternMatchingFailure ->
+              try
+                (* Needed in cases such as pat=([x]T ?) and ty=(T C)
+                   with T reducible against constructor C *)
+                matches weakpat ty 
+              with PatternMatchingFailure ->
+                failwith "caught")
 	  [dFLTty; nf_ty]
       in
       (bindings,dFLT)