-
-(* from ProceduralClasify ***************************************************)
-
-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)
- in
- aux false [] 0 c t
-
-(****************************************************************************)