X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic%2Fcic.ml;h=5495872151bda13625042b884b9c8d77dd0943b3;hb=346c502bf7c78629e75e49f8d9ca379144fdb5df;hp=1becd44428bd3b4f9139c01280e0d47ef48de26e;hpb=1b1c51a6172c0b41b7e5cf01cb0257a60e6f5622;p=helm.git

diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index 1becd4442..549587215 100644
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -62,15 +62,17 @@ type object_flavour =
   | `Remark
   | `Theorem
   | `Variant
+  | `Axiom
   ]
 
 type object_class =
-  [ `Coercion
+  [ `Coercion of int
   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
-  | `Record of (string * bool) list (** 
+  | `Record of (string * bool * int) list (** 
                         inductive type that encodes a record; the arguments are
-                        the record fields names and if they are coercions *)
+                        the record fields names and if they are coercions and
+                        then the coercion arity *)
   | `Projection     (** record projection *)
   ]