From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 20 Jul 2006 15:17:46 +0000 (+0000)
Subject: Revert of the previous situation: when an identifier has no universe all the
X-Git-Tag: make_still_working~7026
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3e654398885c207e9509bb08a2d803c3ee695635;p=helm.git

Revert of the previous situation: when an identifier has no universe all the
passes that does not use the library are doomed to fail and the user will
be asked how to instantiate everyn identifier (not withstanding performances).
Now if an identifier has no universe we look for its interpretations in the
library.
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 85f05aa1c..645ad57ac 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -833,7 +833,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
                     | item -> item
                   in
                   Environment.find item e
-                with Not_found -> [])
+                with Not_found -> lookup_in_library ())
           in
           choices
       in