-let split t =
- let rec aux a n = function
- | C.Prod (_, v, t) -> aux (v :: a) (succ n) t
- | C.Cast (t, v) -> aux a n t
- | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
- | v -> v :: a, n
+let split c t =
+ let add s v c = Some (s, C.Decl v) :: c in
+ let rec aux whd a n c = function
+ | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
+ | v when whd -> v :: a, n
+ | v -> aux true a n c (R.whd ~delta:true c v)