From 59c85666e58d43d1dce56a2456db5f1ec223c1c3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 22 Sep 2006 16:28:39 +0000 Subject: [PATCH] Bug fixed: aliases for numbers were no longer handled correctly (since 0 was a wildcard only for symbols). --- components/cic_disambiguation/disambiguate.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index fbe191416..fb4c338a4 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -717,6 +717,10 @@ let domain_diff dom1 dom2 = (match elt with Symbol (symb',_) when symb = symb' -> true | _ -> false) + | Num i -> + (match elt with + Num _ -> true + | _ -> false) | item -> elt = item ) dom2 in -- 2.39.2