Corrected version od meta_convertibnility_subst.

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 55678ae755d2288ff85d84fd4ebe9020aba29f60..d24c244a75f4f24e26530dd5319229affd2fa0be 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/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/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index e35918c689b805b0e6b4037133e001e9583abe8f..f449d437e91ddb192dfed685e263876af8b1454a 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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 ->