]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/proofEngineReduction.mli
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / proofEngineReduction.mli
index ebb61a7c8bbb54ccf0094d050dfd8cdd8dc8a3a8..67247876aaa2e62f12a2bc5608f6c18f89d71487 100644 (file)
@@ -36,7 +36,7 @@ exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 val alpha_equivalence: Cic.term -> Cic.term -> bool
 val replace :
-  equality:(Cic.term -> 'a -> bool) ->
+  equality:('a -> Cic.term -> bool) ->
   what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val replace_lifting :
   equality:(Cic.term -> Cic.term -> bool) ->