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

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 45fa23a0d01d3bc10329801ffccbb7b313d1c5fc..a835e074f40ff48853d9e957de2b9d5d41d13e21 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -154,6 +154,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
+    | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""