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: make_still_working~6863
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6ccef08d4051b5e1b86049010ba68ed39ee79a6;p=helm.git

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

diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml
index a360dde38..8263fd315 100644
--- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/software/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 =