X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=1c2bf8df0e46d968d703708a33d482ca1e84469d;hb=904ecbd458b20b47d250889459f9aa9ebd26d04d;hp=ba51157ff9f4aa24464733c0820f0b518e4d7119;hpb=8f8d3ad5a02faed2ddcaa22f49a9099175445ef4;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index ba51157ff..1c2bf8df0 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -53,6 +53,15 @@ type name =
  | Name of string
  | Anonymous
 
+type object_flavour =
+  [ `Definition
+  | `Fact
+  | `Lemma
+  | `Remark
+  | `Theorem
+  | `Variant
+  ]
+
 type object_class =
   [ `Coercion
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
@@ -64,6 +73,7 @@ type object_class =
 
 type attribute =
   [ `Class of object_class
+  | `Flavour of object_flavour 
   | `Generated
   ]