in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as

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

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index 9ad05dc926725e75b9ca287ebc4b8e3324ae4a9e..3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,13 +25,14 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
   | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
   | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)