From 7ea5e4e0064e2c66730105af437eb404b0ed1498 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 24 Jul 2006 16:36:26 +0000 Subject: [PATCH] Bug fixed: a symbol alias Symb(s,0) now subsumes the case Symb(s,n) for each n. --- components/cic_disambiguation/disambiguate.ml | 12 +++++++++--- components/cic_disambiguation/disambiguateTypes.ml | 7 +++++++ 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 645ad57ac..cb4d85cfd 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -710,9 +710,15 @@ let domain_of_obj ~context ast = (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) - let is_in_dom2 = - List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt')) - (fun _ -> false) dom2 + let is_in_dom2 elt = + List.exists + (function + | Symbol (symb, 0) -> + (match elt with + Symbol (symb',_) when symb = symb' -> true + | _ -> false) + | item -> elt = item + ) dom2 in List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1 diff --git a/components/cic_disambiguation/disambiguateTypes.ml b/components/cic_disambiguation/disambiguateTypes.ml index 79388f819..a360dde38 100644 --- a/components/cic_disambiguation/disambiguateTypes.ml +++ b/components/cic_disambiguation/disambiguateTypes.ml @@ -55,6 +55,13 @@ struct include Environment' + let find k env = + match k with + Symbol (sym,n) -> + (try find k env + with Not_found -> find (Symbol (sym,0)) env) + | _ -> find k env + let cons k v env = try let current = find k env in -- 2.39.2