X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fcic.ml;h=1b02df3f1a12c7367a64a64cdc49fad3f7d1d9c0;hb=12fe61bed1275c4c596501fb951a9197f50c93e8;hp=20a6cb457dec63c700283ac952204357c38ab0de;hpb=9c9e979d4c45cf3b1ee01688b2c36fe49190ce98;p=helm.git

diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 20a6cb457..1b02df3f1 100644
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -57,6 +57,7 @@ type name =
 
 type object_flavour =
   [ `Definition
+  | `MutualDefinition
   | `Fact
   | `Lemma
   | `Remark
@@ -66,13 +67,15 @@ type object_flavour =
   ]
 
 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 *)
+  | `InversionPrinciple (** inversion principle *)
   ]
 
 type attribute =