| Appl of term list
| Binder of binder_kind * capture_variable * term
| Case of term * string option * term option * (case_pattern * term) list
+ | Cast of term * term
| LetIn of capture_variable * term * term
| LetRec of induction_kind * (capture_variable * term * int) list * term
| Ident of string * subst list option
and subst = string * term
and case_pattern = string * capture_variable list
+(*
let pack asts =
List.fold_right
(fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc))
| Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast]
| Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt
| _ -> assert false
-
+*)