From 14aeb0b894fc5a112519e17eab06256bdaeed864 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 23:36:51 +0000 Subject: [PATCH] just a Pcre expression fixed, nothing real --- helm/software/components/tactics/paramodulation/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)-> -- 2.39.2