[ `Coercion
| `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
- | `Record (** inductive type that encodes a record *)
+ | `Record of string list (** inductive type that encodes a record;
+ the arguments are the record fields *)
| `Projection (** record projection *)
]