From 7e3a07fafe87931279f1c9d4f31aaf9a6f9637d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 29 Sep 2023 13:43:30 +0200 Subject: [PATCH] Remove dead code exception try/catch Dead since class_info returned option AFAICT --- tactics/class_tactics.ml | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0ee20badbfb5..fecf6cf775d1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -257,20 +257,18 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let nprods = List.length prods in let allowed_evars = let all = Evarsolve.AllowedEvars.all in - try - match hdc with - | Some (hd,_) when only_classes -> - begin match Typeclasses.class_info hd with - | Some cl -> - if cl.cl_strict then - let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in - let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - Evarsolve.AllowedEvars.from_pred allowed - else all - | None -> all - end - | _ -> all - with e when CErrors.noncritical e -> all + match hdc with + | Some (hd,_) when only_classes -> + begin match Typeclasses.class_info hd with + | Some cl -> + if cl.cl_strict then + let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in + let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in + Evarsolve.AllowedEvars.from_pred allowed + else all + | None -> all + end + | _ -> all in let tac_of_hint = fun (flags, h) ->