]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: the wrong exception was enriched, breaking the invariant that
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Feb 2006 11:33:05 +0000 (11:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Feb 2006 11:33:05 +0000 (11:33 +0000)
only unlocalized exceptions can be enriched.

helm/software/components/cic_unification/cicRefine.ml

index b74d4029680c7349872672cd4372ec8ba6652c52..52b1a1034d365207a33077155dc58e282c68dabd 100644 (file)
@@ -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 " ^