| LocatedTerm of location * term
| Appl of term list
- | Appl_symbol of string * term list
+ | Appl_symbol of string * int * term list (* literal, args, instance *)
| Binder of binder_kind * Cic.name * term option * term
(* kind, name, type, body *)
| Case of term * string * term option * (case_pattern * term) list
| LetIn of string * term * term (* name, body, where *)
| LetRec of induction_kind * (string * term * term option * int) list * term
(* (name, body, type, decreasing argument) list, where *)
- | Ident of string * subst list
+ | Ident of string * subst list (* literal, substitutions *)
| Meta of int * meta_subst list
- | Num of string
+ | Num of string * int (* literal, instance *)
| Sort of sort_kind
and meta_subst = term option