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

diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 39beb84aa..f8cdec89b 100644
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -34,8 +34,6 @@ exception WrongShape
 exception AlreadySimplified
 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
-val alpha_equivalence: Cic.term -> Cic.term -> bool
-
 (* Replaces "textually" in "where" every term in "what" with the corresponding
    term in "with_what". The terms in "what" ARE NOT lifted when binders are
    crossed. The terms in "with_what" ARE NOT lifted when binders are crossed.
@@ -52,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
@@ -65,7 +64,9 @@ val replace_lifting_csc :
   int -> equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 
-val subst_inv :
+(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]"
+   up to the fact that the index to start from can be specified *)
+val replace_with_rel_1_from :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> int -> Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term