]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content/notationEnv.ml
First commit with new (incomplete) disambiguation engine.
[helm.git] / matitaB / components / content / notationEnv.ml
index be9171a8d9318a714e16fd5ceffbc2a069099278..77ffd92f22b60e9d7fdce05d7949f85f00e1ffb5 100644 (file)
@@ -107,12 +107,12 @@ let declaration_of_var = function
 
 let value_of_term = function
   | Ast.Num (s, _) -> NumValue s
-  | Ast.Ident (s, None) -> StringValue (Var s)
+  | Ast.Ident (s, (* `Ambiguous? *) _) -> StringValue (Var s)
   | t -> TermValue t
 
 let term_of_value = function
-  | NumValue s -> Ast.Num (s, 0)
-  | StringValue (Ident s) -> Ast.Ident (s, None)
+  | NumValue s -> Ast.Num (s, None)
+  | StringValue (Ident s) -> Ast.Ident (s, `Ambiguous)
   | TermValue t -> t
   | _ -> assert false (* TO BE UNDERSTOOD *)