elim tactic: it needs two arguments, a term as well as a pattern

[helm.git] / components / acic_procedural / proceduralPreprocess.mli

diff --git a/components/acic_procedural/proceduralPreprocess.mli b/components/acic_procedural/proceduralPreprocess.mli
index 7bd55f4e221fd09b0dd5f9187fb41b56f875188a..6d66bf23732b2e83575826dd8f929cb10383a443 100644 (file)
--- a/components/acic_procedural/proceduralPreprocess.mli
+++ b/components/acic_procedural/proceduralPreprocess.mli
@@ -23,6 +23,4 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val split: Cic.context -> Cic.term -> Cic.term list * int
-
 val pp_obj: Cic.obj -> Cic.obj