From 1efb99c438c14bbda44f7b8dfe169968a18215a5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 20 Jul 2006 15:17:46 +0000 Subject: [PATCH] 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. --- components/cic_disambiguation/disambiguate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 85f05aa1c..645ad57ac 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/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 -- 2.39.2