From 544a9aee8a26a4d7c613ef8a02f045c53d55f998 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Sep 2009 08:25:33 +0000 Subject: [PATCH] catch wrapped exception --- helm/software/components/ng_tactics/nTacStatus.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 035e65ac7..25beed259 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -239,8 +239,8 @@ let select_term (* we could lift wanted step-by-step *) try true, unify status ctx (None, ctx, t) wanted with - | NCicUnification.UnificationFailure _ - | NCicUnification.Uncertain _ -> false, status + | Error (_, Some (NCicUnification.UnificationFailure _)) + | Error (_, Some (NCicUnification.Uncertain _)) -> false, status in let match_term status ctx (wanted : cic_term) t = let rec aux ctx (status,already_found) t = -- 2.39.2