| `Elim of sort (* elimination principle; universe is not relevant *)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)
+ | `DiscriminationPrinciple (* discrimination principle *)
| `Variant
| `Local
| `Regular ] (* Local = hidden technicality *)
(* inductive type that encodes a record; the arguments are the record
* fields names and if they are coercions and then the coercion arity *)
-type generated = [ `Generated | `Provided ]
+type source = [ `Generated (* generated by matita *)
+ | `Provided (* provided as defined by the user *)
+ | `Implied (* provided as generated by another ITP *)
+ ]
-type c_attr = generated * def_flavour * def_pragma
-type f_attr = generated * def_flavour * def_pragma
-type i_attr = generated * ind_pragma
+type c_attr = source * def_flavour * def_pragma
+type f_attr = source * def_flavour * def_pragma
+type i_attr = source * ind_pragma
(* invariant: metasenv and substitution have disjoint domains *)
type obj_kind =