X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=e4520292df8b9a9e7c489c1cf1876d77caaefb0a;hb=22964c949671af4b5e739b06b915a81a4fc2c5b5;hp=3d54fd18bbc9e126c663b30ab7b1607711a2f389;hpb=ed207660b8a0fa34f1d34b9dbb41144c5be29e68;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 3d54fd18b..e4520292d 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -175,7 +175,7 @@ let replace_tac ~pattern ~with_what =
             ~start:(
               P.cut_tac 
                (C.Appl [
-                 (C.MutInd (LibraryObjects.eq_URI, 0, [])) ;
+                 (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ;
                  ty_of_with_what ; 
                  what ; 
                  with_what]))