From 328a447fe9cbc58758a6279c49a8d9cdb6323745 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 18 Feb 2006 11:33:05 +0000 Subject: [PATCH] Bug fixed: the wrong exception was enriched, breaking the invariant that only unlocalized exceptions can be enriched. --- helm/software/components/cic_unification/cicRefine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index b74d40296..52b1a1034 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/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 " ^ -- 2.39.2