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

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

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index dbdfb979209b146c32ee303f89dbe1f599adb096..d6638b3f07f5f294d227150f2ad908aca997e38e 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -35,6 +35,7 @@ module HObj = HelmLibraryObjects
 module A    = Cic2acic
 module Ut   = CicUtil
 module E    = CicEnvironment
+module PEH  = ProofEngineHelpers
 module PER  = ProofEngineReduction
 
 module P    = ProceduralPreprocess
@@ -275,7 +276,7 @@ and mk_proof st = function
       let script = if proceed then
          let ty = get_type "TC2" st hd in
          let (classes, rc) as h = Cl.classify st.context ty in
-         let premises, _ = P.split st.context ty in
+         let premises, _ = PEH.split_with_whd (st.context, ty) in
         assert (List.length classes - List.length tl = 0);
         let synth = I.S.singleton 0 in
          let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in