(hopefully forever).
in
aux term
+(*
let pack terms =
List.fold_right
(fun term acc -> Cic.Prod (Cic.Anonymous, term, acc))
| Cic.Prod (Cic.Anonymous, term, Cic.Sort (Cic.Type _)) -> [term]
| Cic.Prod (Cic.Anonymous, term, tgt) -> term :: unpack tgt
| _ -> assert false
+*)
let rec strip_prods n = function
| t when n = 0 -> t
val term_of_uri: string -> Cic.term (** @raise UriManager.IllFormedUri *)
val uri_of_term: Cic.term -> string (** @raise Invalid_argument "uri_of_term" *)
+(*
(** packing/unpacking of several terms into a single one *)
val pack: Cic.term list -> Cic.term
val unpack: Cic.term -> Cic.term list
+*)
(** {2 Cic selectors} *)
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
-
+*)
and subst = string * term
and case_pattern = string * capture_variable list
+(*
val pack: term list -> term
val unpack: term -> term list
-
+*)