X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=2544adb5d0deaec128f9d842a0768176f0a61e30;hb=14e2489ae86ecb6467fe9a7ba3b742a8d53c47ea;hp=85f4a3187ea641290d98c2fd75118e15912fedb0;hpb=3b6baca9f28c7d410e543c19f0d8e8467bf25894;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 85f4a3187..2544adb5d 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -94,6 +94,7 @@ let string_of_sort_kind = function
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
   | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
 
 let map_space f l =
  HExtlib.list_concat
@@ -238,7 +239,7 @@ let pp_ast0 t k =
             (fun (params, name, ty, body, rec_param) ->
               [ break;
                 hvbox false true ([
-                  keyword "and";
+                  keyword "and"; space;
                   name] @
                   params @
                   [space; keyword "on" ; space; rec_param ;space ] @