X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationEnv.ml;h=eb85ec038a2623127c69d2414708d8893f94a2a3;hb=b3f366c0fa3fcadcf5f21913f71a2bce591e47d0;hp=986c9b63c84a45ca93fc9e1d979129b42baad14d;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git

diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml
index 986c9b63c..eb85ec038 100644
--- a/matitaB/components/content/notationEnv.ml
+++ b/matitaB/components/content/notationEnv.ml
@@ -54,6 +54,21 @@ type declaration = string * value_type
 type binding = string * (value_type * value)
 type t = binding list
 
+(* let rec pp_value = function
+ | TermValue t -> "T#" ^ NotationPp.pp_term (new NCicPp.status) t
+ | StringValue (Ident i) -> "I#" ^ i
+ | StringValue (Var v) -> "V#" ^ v
+ | NumValue n -> "N#" ^ n
+ | OptValue None -> "O#None"
+ | OptValue (Some v) -> "O#" ^ pp_value v
+ | ListValue vl -> "L#[" ^ (String.concat ";" (List.map pp_value vl)) ^ "]"
+ | DisambiguationValue _ -> "D#"
+
+let pp_binding = function
+ | s, (ty,v) -> Printf.sprintf "{ %s := %s : %s }" s (pp_value v) "..."
+
+let pp_env e = String.concat " " (List.map pp_binding e) *)
+
 let lookup env name =
   try
     List.assoc name env