From bbe533d3f0dd106840af4987242ad7fa10286009 Mon Sep 17 00:00:00 2001 From: Lasse Blaauwbroek Date: Sat, 3 Jun 2023 19:11:14 +0200 Subject: [PATCH] Backport coq/coq#17687 | Catch errors from lib_ref in the logic monad --- tactics/ind_tables.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 2f531f4cc1a6..171edaac436c 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -195,17 +195,21 @@ let find_scheme kind (mind,i as ind) = | Some s -> Proofview.tclUNIT s | None -> - match Hashtbl.find scheme_object_table kind with - | s,IndividualSchemeFunction (f, deps) -> - let deps = match deps with None -> [] | Some deps -> deps (Global.env ()) ind in - let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) Evd.empty_side_effects deps in - let c, eff = define_individual_scheme_base kind s f ~internal:true None ind eff in - Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c - | s,MutualSchemeFunction (f, deps) -> - let deps = match deps with None -> [] | Some deps -> deps (Global.env ()) mind in - let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) Evd.empty_side_effects deps in - let ca, eff = define_mutual_scheme_base kind s f ~internal:true [] mind eff in - Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i) + try + match Hashtbl.find scheme_object_table kind with + | s,IndividualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps (Global.env ()) ind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) Evd.empty_side_effects deps in + let c, eff = define_individual_scheme_base kind s f ~internal:true None ind eff in + Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c + | s,MutualSchemeFunction (f, deps) -> + let deps = match deps with None -> [] | Some deps -> deps (Global.env ()) mind in + let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) Evd.empty_side_effects deps in + let ca, eff = define_mutual_scheme_base kind s f ~internal:true [] mind eff in + Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i) + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e let define_individual_scheme kind names ind = let _ , eff = define_individual_scheme kind ~internal:false names ind in