elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli
index 67247876aaa2e62f12a2bc5608f6c18f89d71487..c0318bdfeb53be8562604f7595fabc77f8d136f5 100644 (file)
--- a/components/tactics/proofEngineReduction.mli
+++ b/components/tactics/proofEngineReduction.mli
@@ -44,6 +44,9 @@ val replace_lifting :
 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
 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