X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;fp=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=bee671ee8ecbdfec342daa090a16638f300143b5;hb=8653d506aacaf019deb3438bd4681ad1000061bd;hp=1bb8ac9550570c0e1883a86a2dbe753cfe10e5e5;hpb=c07a8ba5564610278faed3c86d9a21a9ee0c644e;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 1bb8ac955..bee671ee8 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -28,8 +28,9 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
+(* 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
 
   (** raised when an environment is not enough informative to decide *)
@@ -962,7 +963,7 @@ in refine_profiler.HExtlib.profile foo ()
       try
         let res =
          match aux aliases [] None todo_dom base_univ with
-         | [],errors -> raise (NoWellTypedInterpretation errors)
+         | [],errors -> raise (NoWellTypedInterpretation (0,errors))
          | [_,diff,metasenv,t,ugraph],_ ->
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false