From b89690596acb0b24f1fd45da28ac04b4ad217e98 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Dec 2007 22:01:38 +0000 Subject: [PATCH] Even if the error is not localized, it was not a good idea to make the unification error escape. --- helm/software/components/cic_unification/cicRefine.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 970d3e05f..954c4835b 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1856,10 +1856,13 @@ let typecheck metasenv uri obj ~localization_tbl = " but is here used with type " ^ CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) in - match exn with - RefineFailure _ -> raise (HExtlib.Localized (loc exn,RefineFailure msg)) - | Uncertain _ -> raise (HExtlib.Localized (loc exn,Uncertain msg)) - | _ -> assert false + let exn' = + match exn with + RefineFailure _ -> RefineFailure msg + | Uncertain _ -> Uncertain msg + | _ -> assert false + in + raise (HExtlib.Localized (loc exn',exn')) in let bo' = CicMetaSubst.apply_subst subst bo' in let ty' = CicMetaSubst.apply_subst subst ty' in -- 2.39.2