X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=7893ecba6142ef4a5934d3edc0fd18db3ec51a14;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=e35918c689b805b0e6b4037133e001e9583abe8f;hpb=9ae997cc107e7cacfe3ee62c316361257f3832d4;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index e35918c68..7893ecba6 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 ->
@@ -1223,7 +1223,7 @@ let rec pp_proofterm name t context =
               when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
-              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+              when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
               when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->