Re-added exception, just for now (debugging).

diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
index b8cadbcbf53c738835acec46dfd7148bee4bcaf1..9aa41c52b97761a7eb80960aa54e57d8832811c0 100644 (file)
--- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
+++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+  (DisambiguateTypes.domain_item * string) list *
+  (Stdpp.location * string) Lazy.t * bool) list list
+
 open Printf
 
 let debug = false;;
@@ -79,7 +85,7 @@ let disambiguate_thing ~aliases ~universe
         (try
           set_aliases pass (try_pass pass)
          with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
-          raise (GrafiteDisambiguator.DisambiguationError (offset, errors @ [newerrors])))
+          raise (DisambiguationError (offset, errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)

diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli
index db9671cc4d10b7c34f27b1f1897d53eb33ad5b88..153af12bcc2a4d18c8cd06491aba2b1a8266dc22 100644 (file)
--- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli
+++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli
@@ -11,6 +11,12 @@
 
 (* $Id$ *)
 
+exception DisambiguationError of
+ int *
+ ((Stdpp.location list * string * string) list *
+  (DisambiguateTypes.domain_item * string) list *
+  (Stdpp.location * string) Lazy.t * bool) list list
+
 val disambiguate_term :
   context:NCic.context ->
   metasenv:NCic.metasenv ->