just a Pcre expression fixed, nothing real

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index e35918c689b805b0e6b4037133e001e9583abe8f..7893ecba6142ef4a5934d3edc0fd18db3ec51a14 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 ->
@@ -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)->