X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic%2Fcic.ml;h=ba51157ff9f4aa24464733c0820f0b518e4d7119;hb=e2fb8962f72096d3f0bb19f40b00a3502a11e932;hp=23bb7661b0bb4d8b96340c032f73e67970760656;hpb=f47b833df94d134090a65653077744290438a875;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 23bb7661b..ba51157ff 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -57,7 +57,8 @@ 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 *)
   ]