| Try of 'tactic tactical (* try a tactical and mask failures *)
type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
+type induction_kind = [ `Inductive | `CoInductive ]
+type sort_kind = [ `Prop | `Set | `Type | `CProp ]
type case_pattern = string list
| LocatedTerm of location * term
| Appl of term list
- | Binder of binder_kind * string * term option * term
+ | 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 * term option * (case_pattern * term) list
- (* what to match, case type, <pattern,action> list *)
+ | Case of term * string * term option * (case_pattern * term) list
+ (* what to match, inductive type, out type, <pattern,action> list *)
| LetIn of string * term * term (* name, body, where *)
- | LetRec of (string * term * term option * int) list * term
+ | LetRec of induction_kind * (string * term * term option * int) list * term
(* (name, body, type, decreasing argument) list, where *)
- | Ident of string * subst list
- | Meta of string * meta_subst list
- | Int of int
+ | Ident of string * subst list (* literal, substitutions *)
+ | Meta of int * meta_subst list
+ | Num of string * int (* literal, instance *)
+ | Sort of sort_kind
and meta_subst = term option
and subst = string * term