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

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

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index a2cc0d0e7b04489333cadfb33572aa9b60dfbb49..021fe1c9d676bb59a9a7cfcd6fbc93bcbaa0e35a 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -26,14 +26,26 @@
 (** {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 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 * bool) list
 exception PathNotWellFormed
 
 val interpretate_path :
   context:Cic.name list -> CicNotationPt.term ->
     Cic.term
 
+type 'a disambiguator_input = string * int * 'a
+    
 module type Disambiguator =
 sig
   (** @param fresh_instances when set to true fresh instances will be generated
@@ -47,7 +59,7 @@ sig
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
-    CicNotationPt.term ->
+    CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term *
@@ -61,7 +73,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj ->
+    CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *