]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_acic/cic2acic.ml
- hExtlib: added debugging information for split_nth
[helm.git] / helm / software / components / cic_acic / cic2acic.ml
index 563beaa1c11dd678680e828b02220b78d26f2f70..9ad05dc926725e75b9ca287ebc4b8e3324ae4a9e 100644 (file)
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe  ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType 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 ^ "]"
   | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)