X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=e04b00b7057cbd622fce15ed55daee247e07057b;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=f8b8acba03be7ecbdccc01b94cf8d2dc29cc71df;hpb=7aa0e7901b71a660c6d6f55d96a38a3a9d1d3c7d;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index f8b8acba0..e04b00b70 100644
--- 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 ->