New command default "foo" uri1 ... urin

[helm.git] / helm / ocaml / tactics / equalityTactics.ml

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 3d54fd18bbc9e126c663b30ab7b1607711a2f389..e4520292df8b9a9e7c489c1cf1876d77caaefb0a 100644 (file)
--- 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]))