]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.mli
DisambiguationError exceptions (that have locations inside) are now relocated
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.mli
index fc88b6cf84d54320fb092cb9a3f67763a1585897..a2cc0d0e7b04489333cadfb33572aa9b60dfbb49 100644 (file)
@@ -25,8 +25,9 @@
 
 (** {2 Disambiguation interface} *)
 
+(* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- (Token.flocation option * string Lazy.t) list
int * (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :