*)
module C = Cic
+
+module P = ProceduralPreprocess
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, _ = P.split c t in
+ match rc with
+ | 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)