From e961ace331ec961dcec0e2525d7b9142d04b5154 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 27 Apr 2008 11:16:15 +0000
Subject: - Fix bug in unification not taking into account the right meta
 substitution. Makes unification succeed a bit more often, hence auto works
 better in some cases. - Backtrack the changes of auto using Hint Unfold to do
 more delta and add a new tactic "new auto" which does that, for
 compatibility.

The first fix may have a big impact on the contribs, whereas the second
should make them compile again... we'll see.


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

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 90d6bb081b..216900bdbd 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -148,7 +148,7 @@ let expand_constant env flags c =
 let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
   let nb = nb_rel env in
   let trivial_unify pb (metasubst,_) m n =
-    match subst_defined_metas metas m with
+    match subst_defined_metas metasubst m with
     | Some m ->
 	(match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
@@ -214,9 +214,9 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
 		  let pb = ConvUnderApp (len1,len2) in
 		  array_fold_left2 (unirec_rec curenv topconv true)
 		    (unirec_rec curenv pb true substn f1 f2) l1 l2
-		  with ex when precatchable_exception ex ->
-		    expand curenv pb b substn cM f1 l1 cN f2 l2)
-
+		with ex when precatchable_exception ex ->
+		  expand curenv pb b substn cM f1 l1 cN f2 l2)
+		
 	| _ -> 
 	    let (f1,l1) = 
 	      match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
-- 
cgit v1.2.3