From 730e8b8445c6ff28540aff4a052e19b90159a86d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 9 Jan 2016 17:10:36 +0100 Subject: Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable. --- tactics/autorewrite.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e4ff1c906..dce6f674a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -197,7 +197,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = try_do_hyps (fun id -> id) ids end }) -let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT()) +let auto_multi_rewrite ?(conds=Naive) lems cl = + Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl) let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in @@ -206,7 +207,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = (* autorewrite with .... in clause using tac n'est sur que si clause represente soit le but soit UNE hypothese *) - gen_auto_multi_rewrite conds tac_main lbas cl + Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl) | _ -> Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") -- cgit v1.2.3