matitamake is integrated with matita

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index f8b8acba03be7ecbdccc01b94cf8d2dc29cc71df..fcb42fd1853a869264b9599faf80aa45d98d240e 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -36,12 +36,10 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal l =
-  sprintf "literal(%s)"
-    (match l with
-    | `Symbol s
-    | `Keyword s
-    | `Number s -> s)
+let pp_literal = function
+  | `Symbol s -> sprintf "symbol(%s)" s
+  | `Keyword s -> sprintf "keyword(%s)" s
+  | `Number s -> sprintf "number(%s)" s
 
 let rec pp_term = function
   | AttributedTerm (`Href _, term) when print_attributes ->
@@ -143,6 +141,8 @@ and pp_layout = function
   | Box (box_spec, terms) ->
       sprintf "\\%s [%s]" (pp_box_spec box_spec)
         (String.concat " " (List.map pp_term terms))
+  | Group terms ->
+      sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | List0 (t, sep_opt) ->