X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=7893ecba6142ef4a5934d3edc0fd18db3ec51a14;hb=25e80c6f83850854ed8e8e922fff4e467f8b9924;hp=f449d437e91ddb192dfed685e263876af8b1454a;hpb=2b80cfd9b2f739a28ea9938c4b1fbb7629839d32;p=helm.git

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