X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;fp=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;h=a69ca90abe27206bc7dfbac121d3e6b73f1b03e2;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=50ccb16b47fb6cbaf1cf0c85acc0cfc7841f79f0;hpb=935c8d1b73726bb49b99e5c2dbebdea0d617fa1a;p=helm.git

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 50ccb16b4..a69ca90ab 100644
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -42,15 +42,17 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal =
+(* XXX: ignoring the optional CSYMBOL
+ * (it's fine if this is only used for pretty printing output notations) *)
+let pp_literal (_,t) =
   if debug_printing then
-    (function (* debugging version *)
-      | `Symbol _ as t -> 
+    (match t with (* debugging version *)
+      | `Symbol _ -> 
           sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
-      | `Keyword _ as t -> 
+      | `Keyword _ -> 
           sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
-      | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
-  else NotationUtil.string_of_literal
+      | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+  else NotationUtil.string_of_literal t
 
 let pp_pos =
   function
@@ -271,7 +273,7 @@ and pp_fold_kind = function
 
 and pp_sep_opt = function
   | None -> ""
-  | Some sep -> sprintf " sep %s" (pp_literal sep)
+  | Some sep -> sprintf " sep %s" (pp_literal (None,sep))
 
 and pp_variable = function
   | Ast.NumVar s -> "number " ^ s