diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /plugins/subtac/subtac_obligations.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
-rw-r--r-- | plugins/subtac/subtac_obligations.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index dfcc8526..d8f46098 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -121,7 +121,7 @@ let obl_substitution expand obls deps = let xobl = obls.(x) in let oblb = try get_obligation_body expand xobl - with _ -> assert(false) + with e when Errors.noncritical e -> assert(false) in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) deps [] @@ -498,7 +498,8 @@ let rec solve_obligation prg num tac = let obls = Array.copy obls in let _ = obls.(num) <- obl in let res = try update_obls prg obls (pred rem) - with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e)) + with e when Errors.noncritical e -> + pperror (Errors.print (Cerrors.process_vernac_interp_error e)) in match res with | Remain n when n > 0 -> @@ -552,7 +553,7 @@ and solve_obligation_by_tac prg obls i tac = | Refiner.FailError (_, s) -> user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) | Util.Anomaly _ as e -> raise e - | e -> false + | e when Errors.noncritical e -> false and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in |