New tactic rewrite implemented.

[helm.git] / helm / gTopLevel / proofEngineReduction.mli

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index 06a7f2b9a171b5f10c3b6953a84e66ded811343b..e2d96f40b9d64e6a25ed914c6d031ea9600cfaf3 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -38,5 +38,8 @@ val syntactic_equality : Cic.term -> Cic.term -> bool
 val replace :
   equality:(Cic.term -> 'a -> bool) ->
   what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+val replace_lifting :
+  equality:(Cic.term -> 'a -> bool) ->
+  what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
 val reduce : Cic.context -> Cic.term -> Cic.term
 val simpl : Cic.context -> Cic.term -> Cic.term