From ccb220a27392ef45b5ef8a8493fdba061c14889b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 27 Jun 2016 21:46:03 +0200 Subject: We want tclORELSE to catch exceptions on backtrackings --- tactics/class_tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/class_tactics.ml') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 01c9cda49..3fca7f50d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1217,7 +1217,7 @@ module Search = struct (if Option.is_empty depth then mt() else str" without reaching its limit")) | e -> Proofview.tclZERO ~info:ie e - in Proofview.tclORELSE tac error + in Proofview.tclOR tac error let run_on_evars ?(unique=false) p evm tac = match evars_to_goals p evm with -- cgit v1.2.3