X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=0e4636d572b15d6c1e31939068887f5947b2078c;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=5b5b53f52cd8a3b73edc64f35c7cb7670645157a;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 5b5b53f52..0e4636d57 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -30,7 +30,7 @@ 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