X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_disambiguation%2Fdisambiguate.mli;h=123fcf96928f82fd10f0f43cb3d26b3b30648450;hb=e9b482856904b32a5c92eee8bcd860ffe74fa74f;hp=88162df7bfdff900564f179a1008ad97950c68ac;hpb=9dec56b0dcc55853244fa5ca401c1c19dac3d9d2;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 88162df7b..123fcf969 100644
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -26,8 +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 * ((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 * bool) list
 exception PathNotWellFormed
 
 val interpretate_path :
@@ -63,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 disambiguator_input ->
+    CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *