X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationEnv.mli;h=372bc15e821b4aec68045a062c3cb8683aa131e7;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=858af233c45a2345e05ad7944ea041daca012a5b;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git

diff --git a/matita/components/content/notationEnv.mli b/matita/components/content/notationEnv.mli
index 858af233c..372bc15e8 100644
--- a/matita/components/content/notationEnv.mli
+++ b/matita/components/content/notationEnv.mli
@@ -25,9 +25,13 @@
 
 (** {2 Types} *)
 
+type ident_or_var =
+   Ident of string
+ | Var of string
+
 type value =
   | TermValue of NotationPt.term
-  | StringValue of string
+  | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
@@ -66,7 +70,7 @@ val lookup_value:   t -> string -> value  (** @raise Value_not_found *)
 (** lookup_* functions below may raise Value_not_found and Type_mismatch *)
 
 val lookup_term:    t -> string -> NotationPt.term
-val lookup_string:  t -> string -> string
+val lookup_string:  t -> string -> ident_or_var
 val lookup_num:     t -> string -> string
 val lookup_opt:     t -> string -> value option
 val lookup_list:    t -> string -> value list