]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content/notationEnv.mli
Keeping track of locations of disambiguated ids and symbols.
[helm.git] / matitaB / components / content / notationEnv.mli
index 372bc15e821b4aec68045a062c3cb8683aa131e7..9c83e1a83af465deac37ef0064ec591c5980a35b 100644 (file)
@@ -35,6 +35,7 @@ type value =
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
+  | LocValue of Stdpp.location
 
 type value_type =
   | TermType of int (* the level of the expected term *)
@@ -42,6 +43,7 @@ type value_type =
   | NumType
   | OptType of value_type
   | ListType of value_type
+  | NoType
 
   (** looked up value not found in environment *)
 exception Value_not_found of string