X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineReduction.mli;h=f8cdec89b74956f8e01bcef6bdbddb7529047ae2;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=2d04d39596ea4149042189b2187ffb1245928ebd;hpb=1dd2a5ffce1a935d18372d298e0d85df96ef53bd;p=helm.git

diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 2d04d3959..f8cdec89b 100644
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -50,7 +50,8 @@ val replace :
    inverse of subst up to the fact that free variables in "where" are NOT
    lifted. *)
 val replace_lifting :
-  equality:(Cic.term -> Cic.term -> bool) ->
+  equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
+  context:Cic.context ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 
 (* Replaces in "where" every term in "what" with the corresponding