| `Elim of sort (* elimination principle; universe is not relevant *)
| `Projection (* record projection *)
| `InversionPrinciple (* inversion principle *)
+ | `DiscriminationPrinciple (* discrimination principle *)
| `Variant
| `Local
| `Regular ] (* Local = hidden technicality *)
type obj = NUri.uri * int * metasenv * substitution * obj_kind
(* pretty-printing *)
-class virtual status =
+class virtual status (uid : string option) =
object
+ method user = uid
+
method virtual ppterm: context:context -> subst:substitution ->
metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string