From 7c387703f264666ab83b89b51ee270ff2c7c189c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 13 Sep 2006 11:11:51 +0000
Subject: Abandon unification pattern des evars dans apply: combiné avec le
 backtrack de eauto et le partage des evars entre buts, cela fait davantage de
 choix irréversibles avec rupture de compatibilité. Exemple:    but 1: |- P ?f
    but 2: H1:a=b, H2:c=c, H3:g a = g b |- ?f a = ?f b    eauto sur le but 2
 peut trouver au moins 3 solutions:      1- avec unif premier ordre, il peut
 trouver ?f=g, en appliquant exact H3      2- avec unif pattern, il peut
 trouver ?f=\_.c, en appliquant exact H2      3- en s'y prenant bien, il
 devrait pouvoir laisser ?f ouvert en appliquant         f_equal H1 Dans
 certains exemples (Orsay/FSets/PrecedenceGraph/PrecedenceGraph.v en
 l'occurrence), ajouter l'unif pattern fait adopter la solution 2 plutôt que
 la solution 3. En attente d'un meilleur algorithme, abandon donc de l'unif
 pattern des evars pour apply (ce qui n'empêche pas que, déjà, la situation
 actuelle, qui utilise l'unif premier ordre, peut conduire à faire des mauvais
 choix -- mais au moins on reste compatible...).

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

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index abdf8c863f..30ae394124 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -54,6 +54,7 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
     | Meta k -> 
 	(k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst
     | Evar ev ->
+      (* Currently unused: incompatible with eauto/eassumption backtracking *)
 	metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
     | _ -> assert false
 
@@ -104,10 +105,12 @@ let unify_0 env sigma cv_pb mod_delta m n =
       | _, LetIn (_,b,_,c) -> unirec_rec env pb substn cM (subst1 b c)
 
       | App (f1,l1), App (f2,l2) ->
-	  if is_unification_pattern f1 l1 & not (dependent f1 cN)
+	  if
+	    isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN)
 	  then
 	    solve_pattern_eqn_array env f1 l1 cN substn
-	  else if is_unification_pattern f2 l2 & not (dependent f2 cM)
+	  else if
+	    isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM)
 	  then
 	    solve_pattern_eqn_array env f2 l2 cM substn
 	  else
-- 
cgit v1.2.3