New functorialization: paramod is abstracted over a Orderings.Blob, that is like...

[helm.git] / helm / software / components / tactics / proofEngineReduction.mli

diff --git a/helm/software/components/tactics/proofEngineReduction.mli b/helm/software/components/tactics/proofEngineReduction.mli
index 78f4b7f4c4e8024550fa91dd05a8ae91db2356a6..5bc5f24585326b82d08bc31a17ff3782065abe17 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.mli
+++ b/helm/software/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
@@ -70,6 +69,5 @@ val replace_lifting_csc :
 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
 val simpl : Cic.context -> Cic.term -> Cic.term
 val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term