X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationEnv.ml;h=164fec0e87e52c90b43cd9ea6291f8e686c0033a;hb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a;hp=e95b3ab51d8c29729840ebbf9a5b5702d9252e63;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content/notationEnv.ml b/matita/components/content/notationEnv.ml
index e95b3ab51..164fec0e8 100644
--- a/matita/components/content/notationEnv.ml
+++ b/matita/components/content/notationEnv.ml
@@ -27,9 +27,13 @@
 
 module Ast = NotationPt
 
+type ident_or_var =
+   Ident of string
+ | Var of string
+
 type value =
   | TermValue of Ast.term
-  | StringValue of string
+  | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
@@ -89,7 +93,7 @@ let lookup_list env name =
   | ty, _ -> raise (Type_mismatch (name, ty))
 
 let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
-let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
+let opt_binding_none (n, (ty, _v)) = (n, (OptType ty, OptValue None))
 let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
 let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
 let opt_declaration (n, ty) = (n, OptType ty)
@@ -103,12 +107,12 @@ let declaration_of_var = function
 
 let value_of_term = function
   | Ast.Num (s, _) -> NumValue s
-  | Ast.Ident (s, None) -> StringValue s
+  | Ast.Ident (s, None) -> StringValue (Var s)
   | t -> TermValue t
 
 let term_of_value = function
   | NumValue s -> Ast.Num (s, 0)
-  | StringValue s -> Ast.Ident (s, None)
+  | StringValue (Ident s) -> Ast.Ident (s, None)
   | TermValue t -> t
   | _ -> assert false (* TO BE UNDERSTOOD *)