Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable

[helm.git] / matita / components / content / notationPp.ml

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index e9209d5154e1faf27474ed193f7120472ebf022f..b75192460135beeb4d2286c89ded2d0577af51c7 100644 (file)
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -325,7 +325,8 @@ let pp_obj pp_term = function
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)
-  | Env.StringValue s -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Ident s) -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Var s) -> sprintf "\"${ident %s}\"" s
   | Env.NumValue n -> n
   | Env.OptValue (Some v) -> "Some " ^ pp_value v
   | Env.OptValue None -> "None"