* http://cs.unibo.it/helm/.
*)
-module C = Cic
+module C = Cic
+module PEH = ProofEngineHelpers
-module P = ProceduralPreprocess
module Cl = ProceduralClassify
let is_eliminator = function
- | _ :: C.MutInd _ :: _ -> true
- | _ :: C.Appl (C.MutInd _ :: _) :: _ -> true
- | _ -> false
+ | _ :: (_, C.MutInd _) :: _ -> true
+ | _ :: (_, C.Appl (C.MutInd _ :: _)) :: _ -> true
+ | _ -> false
let is_const = function
| C.Sort _
let bkd c t =
let classes, rc = Cl.classify c t in
- let premises, _ = P.split c t in
+ let premises, _ = PEH.split_with_whd (c, t) in
match rc with
- | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true
+ | Some (i, j, _, _) when i > 1 && i <= List.length classes && is_eliminator premises -> true
| _ ->
- let ts, _ = P.split c t in
- is_appl true (List.hd ts)
+ let _, conclusion = List.hd premises in
+ is_appl true conclusion