type object_flavour =
[ `Definition
+ | `MutualDefinition
| `Fact
| `Lemma
| `Remark
| `Theorem
| `Variant
+ | `Axiom
]
type object_class =
- [ `Coercion
+ [ `Coercion of int
| `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
- | `Record of (string * bool) list (**
+ | `Record of (string * bool * int) list (**
inductive type that encodes a record; the arguments are
- the record fields names and if they are coercions *)
+ the record fields names and if they are coercions and
+ then the coercion arity *)
| `Projection (** record projection *)
+ | `InversionPrinciple (** inversion principle *)
]
type attribute =
(struct
type t = term
let equal = (==)
- let hash = Hashtbl.hash
+ let hash = Hashtbl.hash_param 100 1000
end)
;;