From 49430a1d657ec9521619ea35fe911b598f055df9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 13 Sep 2005 14:36:44 +0000 Subject: [PATCH] New policy for the disambiguation passes. --- helm/matita/matitaDisambiguator.ml | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index db69cb71d..fe9cdca76 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -73,13 +73,14 @@ let disambiguate_thing ~aliases ~(set_aliases: DisambiguateTypes.environment -> 'b -> 'b) (thing: 'a) = - let library = false, DisambiguateTypes.empty_environment in + let library = true, DisambiguateTypes.empty_environment in let multi_aliases = true, aliases in let mono_aliases = false, aliases in let passes = (* *) [ (false, mono_aliases, false); (false, multi_aliases, false); - (true, library, false); + (true, mono_aliases, false); + (true, multi_aliases, false); (true, mono_aliases, true); (true, multi_aliases, true); (true, library, true); @@ -89,15 +90,21 @@ let disambiguate_thing ~aliases CoercDb.use_coercions := use_coercions; f ~fresh_instances ~aliases thing in + let set_aliases (_,(use_multi_aliases,_),_) (_, user_asked as res) = + if not use_multi_aliases then + res + else if user_asked then + res (* one shot aliases *) + else + set_aliases aliases res + in let rec aux = function - | [ pass ] -> try_pass pass + | [ pass ] -> set_aliases pass (try_pass pass) | hd :: tl -> (try - try_pass hd - with Disambiguate.NoWellTypedInterpretation -> - let (_, user_asked) as res = aux tl in - if user_asked then res else set_aliases aliases res) + set_aliases hd (try_pass hd) + with Disambiguate.NoWellTypedInterpretation -> aux tl) | [] -> assert false in let saved_use_coercions = !CoercDb.use_coercions in -- 2.39.2