From 19e7a086a4efbb59452b10ed71f4914e92eb8986 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 26 Nov 2008 17:24:36 +0000 Subject: [PATCH] Re-added exception, just for now (debugging). --- .../components/ng_disambiguation/nGrafiteDisambiguator.ml | 8 +++++++- .../ng_disambiguation/nGrafiteDisambiguator.mli | 6 ++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml index b8cadbcbf..9aa41c52b 100644 --- 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 db9671cc4..153af12bc 100644 --- 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 -> -- 2.39.2