* http://cs.unibo.it/helm/.
*)
-module C = Cic
+module C = Cic
+module PEH = ProofEngineHelpers
+
module Cl = ProceduralClassify
+let is_eliminator = function
+ | _ :: (_, C.MutInd _) :: _ -> true
+ | _ :: (_, C.Appl (C.MutInd _ :: _)) :: _ -> true
+ | _ -> false
+
let is_const = function
| C.Sort _
| C.Const _
| _ -> false
let bkd c t =
- let ts, _ = Cl.split c t in
- is_appl true (List.hd ts)
+ let classes, rc = Cl.classify 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
+ | _ ->
+ let _, conclusion = List.hd premises in
+ is_appl true conclusion