]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic_disambiguation/disambiguate.mli
- Disambiguation error exception enriched with more information
[helm.git] / helm / software / components / cic_disambiguation / disambiguate.mli
index 88162df7bfdff900564f179a1008ad97950c68ac..4a8f90b00303eeb771c6cb15e5739992e1ca3e78 100644 (file)
 
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
- int * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
+ int *
+ ((Token.flocation list * string * string) list *
+  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :