X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fcic.ml;h=1b02df3f1a12c7367a64a64cdc49fad3f7d1d9c0;hb=a9be219c90cccb6c19abbbf3bdf8b806810d2d5c;hp=5495872151bda13625042b884b9c8d77dd0943b3;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git

diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 549587215..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
@@ -74,6 +75,7 @@ type object_class =
                         the record fields names and if they are coercions and
                         then the coercion arity *)
   | `Projection     (** record projection *)
+  | `InversionPrinciple (** inversion principle *)
   ]
 
 type attribute =