X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.mli;h=67247876aaa2e62f12a2bc5608f6c18f89d71487;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=ebb61a7c8bbb54ccf0094d050dfd8cdd8dc8a3a8;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli index ebb61a7c8..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) ->