generalize no more required before elim

[helm.git] / helm / software / components / cic_acic / cic2acic.mli

diff --git a/helm/software/components/cic_acic/cic2acic.mli b/helm/software/components/cic_acic/cic2acic.mli
index e6379283d61f98b173154cd4d256e08a70a667f0..c3cf56e889974b56bd9c03695c3ce8dd4ed140f1 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.mli
+++ b/helm/software/components/cic_acic/cic2acic.mli
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotEnoughElements
+exception NotEnoughElements of string
 
 val source_id_of_id : string -> string
 
@@ -31,7 +31,7 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe]
 
 val string_of_sort: sort_kind -> string
 (*val sort_of_string: string -> sort_kind*)