* fields names and if they are coercions and then the coercion arity *)
type source = [ `Generated (* generated by matita *)
- | `Provided (* provided by the user directly or from another ITP *)
+ | `Provided (* provided as defined by the user *)
| `Implied (* provided as generated by another ITP *)
]