attributes now in the proof status: commit 2

[helm.git] / helm / software / components / cic / cic.ml

diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 5495872151bda13625042b884b9c8d77dd0943b3..c5a5c1e4079991118daf4110fa7fef1c8a785c62 100644 (file)
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -74,6 +74,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 =