experimental classification of disambiguation error, so that supposedly non significa...

[helm.git] / components / cic_disambiguation / disambiguate.mli

diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 4a8f90b00303eeb771c6cb15e5739992e1ca3e78..021fe1c9d676bb59a9a7cfcd6fbc93bcbaa0e35a 100644 (file)
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -26,11 +26,18 @@
 (** {2 Disambiguation interface} *)
 
 (* the integer is an offset to be added to each location *)
+(* list of located error messages, each list is a tuple:
+  * - environment in string form
+  * - environment patch
+  * - location
+  * - error message
+  * - significancy of the error message, if false the error is likely to be
+  *   useless for the final user ... *)
 exception NoWellTypedInterpretation of
  int *
  ((Token.flocation list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t) list
+  Token.flocation option * string Lazy.t * bool) list
 exception PathNotWellFormed
 
 val interpretate_path :