]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_acic/cic2acic.mli
Inverters/Inversion:
[helm.git] / helm / software / components / cic_acic / cic2acic.mli
index 4526521fbd0e6d00f6e57d0b0eb6f05ab8636c09..0bf874e86fd45ae6bab8564d1ea98ed3b271b59e 100644 (file)
@@ -31,7 +31,7 @@ type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
 
-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 | `NCProp of string]
 
 val string_of_sort: sort_kind -> string
 (*val sort_of_string: string -> sort_kind*)