(* what to match, inductive type, out type, <pattern,action> list *)
| Cast of term * term
| 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 *)
+ | LetRec of induction_kind * (capture_variable list * capture_variable * term * int) list * term
+ (* (params, name, body, decreasing arg) list, where *)
| Ident of string * subst list option
(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
type 'term inductive_type = string * bool * 'term * (string * 'term) list
type obj =
- | Inductive of (string * term) list * term inductive_type list
+ | Inductive of capture_variable list * term inductive_type list
(** parameters, list of loc * mutual inductive types *)
| Theorem of Cic.object_flavour * string * term * term option
(** flavour, name, type, body
* will be given in proof editing mode using the tactical language,
* unless the flavour is an Axiom
*)
- | Record of (string * term) list * string * term * (string * term * bool) list
+ | Record of capture_variable list * string * term * (string * term * bool * int) list
(** left parameters, name, type, fields *)
(** {2 Standard precedences} *)