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