Backport coq#17687 | Catch errors from lib_ref in the logic monad

LasseBlaauwbroek · Oct 17, 2023 · bbe533d · bbe533d
1 parent 59425c3
commit bbe533d
Showing 1 changed file with 15 additions and 11 deletions.
diff --git 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