new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[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 1058a48cca4a0faaa09ee2609d4f10a9dc522b08..6131a7dafeb81a7481138919dc4415cdbf171740 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -224,7 +224,9 @@ let ppmetaattrs =
     String.concat ","
      (List.map
        (function
-           `IsSort -> "sort"
+         | `IsTerm -> "term"
+         | `IsType -> "type"
+         | `IsSort -> "sort"
          | `Name n -> "name=" ^ n
          | `InScope -> "in_scope"
          | `OutScope n -> "out_scope:" ^ string_of_int n