diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-09 17:10:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-09 17:11:03 +0100 |
| commit | 730e8b8445c6ff28540aff4a052e19b90159a86d (patch) | |
| tree | 4b247c01cee21075a9e492522bb2d0e9b3122dfd /tactics/autorewrite.ml | |
| parent | 418dceeea548a40c6e00b09aa99267a82949c70c (diff) | |
Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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.") |