X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=d19914ab4166bf423a6cee37caf689a75f414fdb;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=0d78c4971bd90ff46364aaef74dc6330d78b4f7d;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicPp.ml b/matitaB/components/ng_kernel/nCicPp.ml
index 0d78c4971..d19914ab4 100644
--- a/matitaB/components/ng_kernel/nCicPp.ml
+++ b/matitaB/components/ng_kernel/nCicPp.ml
@@ -141,7 +141,7 @@ let ppterm status ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t
       let _,_,t,_ = List.assoc n subst in
       let hd = NCicSubstitution.subst_meta status lc t in
       aux ctx 
-        (NCicReduction.head_beta_reduce (status :> NCic.status) ~upto:(List.length args)
+        (NCicReduction.head_beta_reduce (status :> NCicEnvironment.status) ~upto:(List.length args)
           (match hd with
           | NCic.Appl l -> NCic.Appl (l@args)
           | _ -> NCic.Appl (hd :: args)))
@@ -280,6 +280,7 @@ let string_of_pragma = function
   | `Elim _sort -> "Elim _"
   | `Projection -> "Projection"
   | `InversionPrinciple -> "InversionPrinciple"
+  | `DiscriminationPrinciple -> "DiscriminationPrinciple"
   | `Variant -> "Variant"
   | `Local -> "Local"
   | `Regular -> "Regular"
@@ -359,9 +360,17 @@ let ppsubst status ~metasenv ?use_subst subst =
 
 let ppobj status obj = on_buffer (ppobj status) obj;;
 
-class status =
+class type cstatus =
+  object
+    inherit NCicEnvironment.status
+    inherit NCic.cstatus
+  end
+
+class status (uid : string option) =
  object(self)
+  inherit NCicEnvironment.status uid
   (* this method is meant to be overridden in ApplyTransformation *)
+  method user = uid
   method ppterm = ppterm self
   method ppcontext = ppcontext self
   method ppmetasenv = ppmetasenv self