X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=f449d437e91ddb192dfed685e263876af8b1454a;hb=935efd051844dd7877207c7917eb73016b7c8bc5;hp=e35918c689b805b0e6b4037133e001e9583abe8f;hpb=37177f827ce843b30fb882fc39ecc674c1195d3d;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index e35918c68..f449d437e 100644
--- 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 ->