From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 2 Sep 2009 08:56:04 +0000 (+0000)
Subject: decent error on interpretation declaration
X-Git-Tag: make_still_working~3510
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4b2d1c460f051572d30900ef9014e6ca7fca8c6;p=helm.git

decent error on interpretation declaration
---

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index 12200193e..54c5985f3 100644
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -142,7 +142,9 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
               prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ 
                (DisambiguateTypes.string_of_domain_item item));
 	      dump_aliases prerr_endline "" sstatus;
-              assert false
+              raise (Failure (
+                      (DisambiguateTypes.string_of_domain_item item) ^ 
+                      " not found"));
 	    end
        | p -> p
      in