]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 6806713a4e9375a4c20ca4009d666c54d62720ea..70acd56d8fc15730e8a40564c7d6bb201a1a62a1 100644 (file)
@@ -358,6 +358,9 @@ let pp_command ~term_pp ~obj_pp = function
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value
   | NObj (_,o) -> "not supported"
+  | NUnivConstraint (_) -> "not supported"
+  | NQed (_) -> "not supported"
+  | Pump (_) -> "not supported"
 
 let pp_punctuation_tactical =
   function