From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 25 Sep 2006 14:04:33 +0000 (+0000)
Subject: Bug fixed: a number alias Num 0 now subsumes the case Num n for each n.
X-Git-Tag: 0.4.95@7852~1003
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3314368624a591c3f567d27d6cba505defec72c9;p=helm.git

Bug fixed: a number alias Num 0 now subsumes the case Num n for each n.
---

diff --git a/components/cic_disambiguation/disambiguateTypes.ml b/components/cic_disambiguation/disambiguateTypes.ml
index a360dde38..8263fd315 100644
--- a/components/cic_disambiguation/disambiguateTypes.ml
+++ b/components/cic_disambiguation/disambiguateTypes.ml
@@ -60,6 +60,9 @@ struct
       Symbol (sym,n) ->
        (try find k env
         with Not_found -> find (Symbol (sym,0)) env)
+    | Num n ->
+       (try find k env
+        with Not_found -> find (Num 0) env)
     | _ -> find k env
 
   let cons k v env =