X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.mli;h=67247876aaa2e62f12a2bc5608f6c18f89d71487;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=02e56ba6a207224e38bfa479673f8f01372df2d0;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index 02e56ba6a..67247876a 100644
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -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) ->
@@ -46,3 +46,4 @@ val replace_lifting_csc :
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term
+val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term