| LetIn of capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (capture_variable * term * int) list * term
(* (name, body, decreasing argument) list, where *)
- | Ident of string * subst list (* literal, substitutions *)
+ | Ident of string * subst list option
+ (* literal, substitutions.
+ * Some [] -> user has given an empty explicit substitution list
+ * None -> user has given no explicit substitution list *)
| Implicit
| Meta of int * meta_subst list
| Num of string * int (* literal, instance *)