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 85f05aa1c8700048224840ed34f262f21e0e29f8..645ad57accf85ec211859a23f6954fb1ca494c57 100644 (file)
--- 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