Added an almost working version of Generalize tactic.

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

diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli
index f185dd6638d9a3eaf30bf078039d1cadbf40d207..91bce1a39d3d10b10031c667aae35e43f9e542aa 100644 (file)
--- a/helm/gTopLevel/proofEngineReduction.mli
+++ b/helm/gTopLevel/proofEngineReduction.mli
@@ -40,5 +40,8 @@ val replace :
 val replace_lifting :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term
+val replace_lifting_csc :
+  int -> equality:(Cic.term -> Cic.term -> bool) ->
+  what:Cic.term -> 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