]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/termContentPres.ml
- Procedural: more support for the Debug inline option (does not work yet)
[helm.git] / helm / software / components / content_pres / termContentPres.ml
index 85f4a3187ea641290d98c2fd75118e15912fedb0..2544adb5d0deaec128f9d842a0768176f0a61e30 100644 (file)
@@ -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 ] @