X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineReduction.mli;h=39beb84aa8d8fc55913989f2a97a475ba07f563e;hb=bccb5e2838b8552896ee797af5114e7c7ca037b6;hp=c0318bdfeb53be8562604f7595fabc77f8d136f5;hpb=8ae990161006978a019f0afda4ff8d56a78d1fd0;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineReduction.mli b/helm/software/components/tactics/proofEngineReduction.mli
index c0318bdfe..39beb84aa 100644
--- a/helm/software/components/tactics/proofEngineReduction.mli
+++ b/helm/software/components/tactics/proofEngineReduction.mli
@@ -35,15 +35,36 @@ 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.
+   Every free variable in "where" IS NOT lifted by nnn. *)
 val replace :
   equality:('a -> Cic.term -> bool) ->
   what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
+
+(* Replaces in "where" every term in "what" with the corresponding
+   term in "with_what". The terms in "what" ARE lifted when binders are
+   crossed. The terms in "with_what" ARE lifted when binders are crossed.
+   Every free variable in "where" IS NOT lifted by nnn.
+   Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
+   inverse of subst up to the fact that free variables in "where" are NOT
+   lifted. *)
 val replace_lifting :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
+
+(* Replaces 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 lifted when binders are crossed.
+   Every free variable in "where" IS lifted by nnn.
+   Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
+   inverse of subst up to the fact that "what" terms are NOT lifted. *)
 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 :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term list -> int -> Cic.term -> Cic.term