]> matita.cs.unibo.it Git - helm.git/commitdiff
just a Pcre expression fixed, nothing real
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:36:51 +0000 (23:36 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 8 Sep 2007 23:36:51 +0000 (23:36 +0000)
helm/software/components/tactics/paramodulation/equality.ml

index f449d437e91ddb192dfed685e263876af8b1454a..7893ecba6142ef4a5934d3edc0fd18db3ec51a14 100644 (file)
@@ -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)->