X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;h=50ccb16b47fb6cbaf1cf0c85acc0cfc7841f79f0;hb=10b08809fd7b78ff21f020911b7ec383eb4f1f0d;hp=d120fde68f696587fe6ffb160ed346ae4dd05264;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index d120fde68..50ccb16b4 100644
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -45,14 +45,12 @@ let pp_binder = function
 let pp_literal =
   if debug_printing then
     (function (* debugging version *)
-      | `Symbol s -> sprintf "symbol(%s)" s
-      | `Keyword s -> sprintf "keyword(%s)" s
-      | `Number s -> sprintf "number(%s)" s)
-  else
-    (function
-      | `Symbol s
-      | `Keyword s
-      | `Number s -> s)
+      | `Symbol _ as t -> 
+          sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+      | `Keyword _ as t -> 
+          sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+      | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+  else NotationUtil.string_of_literal
 
 let pp_pos =
   function
@@ -184,10 +182,6 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Ident _    -> t_pp
     | _                    -> sprintf "(%s)" t_pp
 
-and pp_subst status (name, term) =
- sprintf "%s \\Assign %s" name (pp_term status term)
-and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
-
 and pp_pattern status =
  function
     Ast.Pattern (head, href, vars), term ->
@@ -347,7 +341,7 @@ let rec pp_value (status: #NCic.status) = function
   | Env.OptValue (Some v) -> "Some " ^ pp_value status v
   | Env.OptValue None -> "None"
   | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l))
-  | Env.LocValue l -> sprintf "#"
+  | Env.DisambiguationValue _ -> sprintf "#"
 
 let rec pp_value_type =
   function