*** empty log message ***

[helm.git] / helm / ocaml / cic / cic.ml

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 23bb7661b0bb4d8b96340c032f73e67970760656..1c2bf8df0e46d968d703708a33d482ca1e84469d 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -53,16 +53,27 @@ 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
                       * not relevant *)
-  | `Record         (** inductive type that encodes a record *)
+  | `Record of string list (** inductive type that encodes a record;
+                               the arguments are the record fields *)
   | `Projection     (** record projection *)
   ]
 
 type attribute =
   [ `Class of object_class
+  | `Flavour of object_flavour 
   | `Generated
   ]