Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / components / content / notationEnv.ml

diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml
index 77ffd92f22b60e9d7fdce05d7949f85f00e1ffb5..cca2e37998e197b2ca8416762524c918ade43746 100644 (file)
--- a/matitaB/components/content/notationEnv.ml
+++ b/matitaB/components/content/notationEnv.ml
@@ -32,18 +32,20 @@ type ident_or_var =
  | Var of string
 
 type value =
-  | TermValue of Ast.term
+  | TermValue of NotationPt.term
   | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
+  | LocValue of Stdpp.location
 
 type value_type =
-  | TermType of int
+  | TermType of int (* the level of the expected term *)
   | StringType
   | NumType
   | OptType of value_type
   | ListType of value_type
+  | NoType
 
 exception Value_not_found of string
 exception Type_mismatch of string * value_type