severe bug found in parallel zeta

[helm.git] / matitaB / components / ng_kernel / nCic.ml

diff --git a/matitaB/components/ng_kernel/nCic.ml b/matitaB/components/ng_kernel/nCic.ml
index 7e4e4f85535dfd76beb667fa2bc475325a699438..c08f4ed04ee11cfbe4fe60c09c2488522e89a0bf 100644 (file)
--- a/matitaB/components/ng_kernel/nCic.ml
+++ b/matitaB/components/ng_kernel/nCic.ml
@@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *)
   | `Elim of sort       (* elimination principle; universe is not relevant *)
   | `Projection         (* record projection *)
   | `InversionPrinciple (* inversion principle *)
+  | `DiscriminationPrinciple (* discrimination principle *)
   | `Variant 
   | `Local 
   | `Regular ]            (* Local = hidden technicality *)
@@ -121,8 +122,10 @@ type obj_kind =
 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