]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/termContentPres.ml
Added new syntax Type[n] where n is a number.
[helm.git] / helm / software / components / content_pres / termContentPres.ml
index e15442970a0ac3a139d54cf2cf0b1d85d2c1ee95..d6694cbb66419be45f3c88609c12f6434e4eef62 100644 (file)
@@ -93,6 +93,7 @@ let string_of_sort_kind = function
   | `Set -> "Set"
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
+  | `NType s -> "Type[" ^ s ^ "]"
 
 let pp_ast0 t k =
   let rec aux =