X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2Fcic.ml;h=9a4f4b0dedde0fefe8ad8db133207c88804a7af0;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=53b4ef62bc3050c9264e4c4cc8cd5fd97ef90603;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git

diff --git a/helm/software/components/cic/cic.ml b/helm/software/components/cic/cic.ml
index 53b4ef62b..9a4f4b0de 100644
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -67,8 +67,7 @@ type object_flavour =
   ]
 
 type object_class =
-  [ `Coercion of int
-  | `Elim of sort   (** elimination principle; if sort is Type, the universe is
+  [ `Elim of sort   (** elimination principle; if sort is Type, the universe is
                       * not relevant *)
   | `Record of (string * bool * int) list (** 
                         inductive type that encodes a record; the arguments are