- further simplifications (??) of the status dependencies

[helm.git] / matita / components / disambiguation / disambiguate.ml

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 5b5b53f52cd8a3b73edc64f35c7cb7670645157a..8be47f06313688268623d958ff724c68264e7ebc 100644 (file)
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -28,9 +28,8 @@
 open Printf
 
 open DisambiguateTypes
-open UriManager
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 
 (* the integer is an offset to be added to each location *)
 exception Ambiguous_input