pattern:ProofEngineTypes.lazy_pattern ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
[ `Decl of (Cic.context * Cic.term) list
- | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option
+ | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list
] option list *
(Cic.context * Cic.term) list
t and t_i is the premise of t accessed by Rel i in t_0.
Performes a whd on the conclusion before giving up.
Each t_i is returned with a context c_i in wich it is typed
+ split_with_normalize (c, t) normalizes t before operating the split
+ whd is useless here
*)
val split_with_whd: Cic.context * Cic.term ->
(Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term ->
+ (Cic.context * Cic.term) list * int