Prop
| Set
| Type of CicUniv.universe
- | CProp
+ | CProp of CicUniv.universe
type name =
| Name of string
]
type object_class =
- [ `Coercion of int
- | `Elim of sort (** elimination principle; if sort is Type, the universe is
+ [ `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
| `Record of (string * bool * int) list (**
inductive type that encodes a record; the arguments are
| Cast of term * term (* value, type *)
| Prod of name * term * term (* binder, source, target *)
| Lambda of name * term * term (* binder, source, target *)
- | LetIn of name * term * term (* binder, term, target *)
+ | LetIn of name * term * term * term (* binder, term, type, target *)
| Appl of term list (* arguments *)
| Const of UriManager.uri * (* uri, *)
term explicit_named_substitution (* explicit named subst. *)
| ACast of id * annterm * annterm (* value, type *)
| AProd of id * name * annterm * annterm (* binder, source, target *)
| ALambda of id * name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * name * annterm * annterm (* binder, term, target *)
+ | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *)
| AAppl of id * annterm list (* arguments *)
| AConst of id * UriManager.uri * (* uri, *)
annterm explicit_named_substitution (* explicit named subst. *)
and context_entry = (* A declaration or definition *)
Decl of term
- | Def of term * term option (* body, type (if known) *)
+ | Def of term * term (* body, type *)
and hypothesis =
(name * context_entry) option (* None means no more accessible *)
and anncontext_entry = (* A declaration or definition *)
ADecl of annterm
- | ADef of annterm
+ | ADef of annterm * annterm
and annhypothesis =
id * (name * anncontext_entry) option (* None means no more accessible *)