From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 18 Feb 2006 11:33:05 +0000 (+0000)
Subject: Bug fixed: the wrong exception was enriched, breaking the invariant that
X-Git-Tag: 0.4.95@7852~1657
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33e92183dbdc1f2bf37a22dde9e1084b2df3a5c8;p=helm.git

Bug fixed: the wrong exception was enriched, breaking the invariant that
only unlocalized exceptions can be enriched.
---

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index b74d40296..52b1a1034 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1174,7 +1174,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                                 newhety s ugraph
                             in
                              newt, subst, metasenv, ugraph
-                           with exn ->
+                           with _ ->
                             enrich localization_tbl hete
                              ~f:(fun _ ->
                                (lazy ("The term " ^