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

[helm.git] / components / acic_procedural / proceduralClassify.ml

diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml
index 2fd2d979d7053abecb185562b9567858df3e6b8c..d21c14601f5108502d27de3c34f1511e3b89c3ab 100644 (file)
--- a/components/acic_procedural/proceduralClassify.ml
+++ b/components/acic_procedural/proceduralClassify.ml
@@ -23,11 +23,10 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module C = Cic
-module D = Deannotate
-module I = CicInspect
-
-module P = ProceduralPreprocess
+module C   = Cic
+module D   = Deannotate
+module I   = CicInspect
+module PEH = ProofEngineHelpers
 
 type conclusion = (int * int) option
 
@@ -57,15 +56,15 @@ let out_table b =
 let id x = x
 
 let classify_conclusion = function
-   | C.Rel i                -> Some (i, 0)
-   | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
-   | _                      -> None
+   | _, C.Rel i                -> Some (i, 0)
+   | _, C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
+   | _                         -> None
 
 let classify c t =
 try   
-   let vs, h = P.split c t in
+   let vs, h = PEH.split_with_whd (c, t) in
    let rc = classify_conclusion (List.hd vs) in
-   let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
+   let map (b, h) (_, v) = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in
    let l, h = List.fold_left map ([], 0) vs in
    let b = Array.of_list (List.rev l) in
    let mk_closure b h =