made executable again

[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 5dd8455ea7a29cb1e7b6a067066f1933b119d164..9a4f4b0dedde0fefe8ad8db133207c88804a7af0 100644 (file)
--- a/helm/software/components/cic/cic.ml
+++ b/helm/software/components/cic/cic.ml
@@ -49,7 +49,7 @@ type sort =
    Prop
  | Set
  | Type of CicUniv.universe
- | CProp
+ | CProp of CicUniv.universe
 
 type name =
  | Name of string
@@ -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