X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCic.ml;h=94dc827c810df412dc5d3c4a5a545885bc5a8058;hb=b41bbbe640d020d2c3ac59cd0398464cd7cf7e41;hp=4490ee0485c218a4b7681d5c3c0048c45198abd9;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 4490ee048..94dc827c8 100644
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -87,13 +87,14 @@ type inductiveType =
  (* relevance, typename, arity, constructors *)
 
 type def_flavour = (* presentational *)
-  [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
+  [ `Axiom | `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
 
 type def_pragma = (* pragmatic of the object *)
   [ `Coercion of int
   | `Elim of sort       (* elimination principle; universe is not relevant *)
   | `Projection         (* record projection *)
   | `InversionPrinciple (* inversion principle *)
+  | `DiscriminationPrinciple (* discrimination principle *)
   | `Variant 
   | `Local 
   | `Regular ]            (* Local = hidden technicality *)
@@ -119,3 +120,38 @@ type obj_kind =
 
  (* the int must be 0 if the object has no body *)
 type obj = NUri.uri * int * metasenv * substitution * obj_kind
+
+(* pretty-printing *)
+class virtual status =
+ object
+  method virtual ppterm: context:context -> subst:substitution ->
+   metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
+
+  method virtual ppcontext: ?sep:string -> subst:substitution ->
+   metasenv:metasenv -> context -> string 
+
+  method virtual ppmetasenv: subst:substitution -> metasenv -> string
+
+  method virtual ppsubst: metasenv:metasenv -> ?use_subst:bool -> substitution -> string
+
+  method virtual ppobj: obj -> string
+ end
+
+(* pretty-printing: same as vstatus, but all methods are concrete         *)
+(* used only to declare concrete instances of subclasses of vstatus class *)
+class type cstatus =
+ object
+  inherit status
+
+  method ppterm: context:context -> subst:substitution ->
+   metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
+
+  method ppcontext: ?sep:string -> subst:substitution ->
+   metasenv:metasenv -> context -> string 
+
+  method ppmetasenv: subst:substitution -> metasenv -> string
+
+  method ppsubst: metasenv:metasenv -> ?use_subst:bool -> substitution -> string
+
+  method ppobj: obj -> string
+ end