Added initial support for inversion principles in Matita NG.

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index 12227b4b190126414e97210547faf4625781db42..ddecb4dfb9ba75c299211307787ce68e27363de3 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -57,6 +57,7 @@ let string_of_implicit_annotation = function
   | `Closed -> "▪"
   | `Type -> ""
   | `Hole -> "□"
+  | `Tagged s -> "[\"" ^ s ^ "\"]"
   | `Term -> "Term"
   | `Typeof x -> "Ty("^string_of_int x^")"
   | `Vector -> "…"