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: 0.4.95@7852~1009
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=59c85666e58d43d1dce56a2456db5f1ec223c1c3;p=helm.git

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

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