From dd4b01b7fbd69a4af86ec5d41eb5da39a27e4a64 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 29 May 2007 09:26:02 +0000
Subject: [PATCH] Corrected version od meta_convertibnility_subst.

---
 components/tactics/auto.ml                    | 13 +++++++------
 components/tactics/paramodulation/equality.ml |  4 ++--
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 55678ae75..d24c244a7 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -1217,24 +1217,25 @@ let prunable ty todo =
 let prunable menv subst ty todo =
   let rec aux = function
     | (S(_,k,_,_))::tl ->
-	(match Equality.meta_convertibility_subst k ty menv with
+	 (match Equality.meta_convertibility_subst k ty menv with
 	  | None -> aux tl
-	  | Some variant -> no_progress variant tl (* || aux tl)*) )
+	  | Some variant -> 
+	       no_progress variant tl (* || aux tl*))
     | (D (_,_,T))::tl -> aux tl
     | _ -> false
   and no_progress variant = function
     | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
     | D ((n,_,P) as g)::tl -> 
 	(match calculate_goal_ty g subst menv with
-           | None -> no_progress subst tl
+           | None -> no_progress variant tl
            | Some (_, gty) -> 
 	       (match calculate_goal_ty g variant menv with
 		  | None -> assert false
-		  | Some (_, gty') ->  
+		  | Some (_, gty') ->
 		      if gty = gty' then
-			no_progress variant tl
+			 no_progress variant tl
 		      else false))
-    | _::tl -> no_progress subst tl
+    | _::tl -> no_progress variant tl
   in
     aux todo
 
diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index e35918c68..f449d437e 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -1050,13 +1050,13 @@ let meta_convertibility_subst t1 t2 menv =
 	       let (_,c,t) = CicUtil.lookup_meta x menv in
 	       let irl = 
 		 CicMkImplicit.identity_relocation_list_for_metavariable c in
-	       (x,(c,Cic.Meta(y,irl),t))
+	       (y,(c,Cic.Meta(x,irl),t))
 	     with CicUtil.Meta_not_found _ ->
 	       try 
 		 let (_,c,t) = CicUtil.lookup_meta y menv in
 		 let irl =  
 		   CicMkImplicit.identity_relocation_list_for_metavariable c in
-		   (y,(c,Cic.Meta(x,irl),t))
+		   (x,(c,Cic.Meta(y,irl),t))
 	       with CicUtil.Meta_not_found _ -> assert false) l in   
 	Some subst
     with NotMetaConvertible ->
-- 
2.39.2