From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 22 Sep 2006 16:28:39 +0000 (+0000)
Subject: Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
X-Git-Tag: make_still_working~6869
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b453fb080b106df17ac71f7afffe50bbf631e1d;p=helm.git

Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index fbe191416..fb4c338a4 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/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