diff options
| author | Gaëtan Gilbert | 2020-07-10 14:11:40 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-13 11:13:07 +0200 |
| commit | 8641cb7385ee8a968e30bc7b9ce263f451a2323e (patch) | |
| tree | dcd90747a9c1b9169b9f56df2dbed7f9e5ef8a33 | |
| parent | f4593ab277c12eda7e000011eeb2276716ac9a09 (diff) | |
Don't catch anomalies for evarconv "cannot find an instance" error
| -rw-r--r-- | pretyping/evarconv.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 400acc25b6..2feae8cc25 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1334,6 +1334,12 @@ let thin_evars env sigma sign c = let c' = applyrec (env,0) c in (!sigma, c') +exception NotFoundInstance of exn +let () = CErrors.register_handler (function + | NotFoundInstance e -> + Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e) + | _ -> None) + let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in @@ -1478,7 +1484,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> instantiate_evar evar_unify flags env_rhs evd ev vid | _ -> evd) - with e -> user_err (Pp.str "Cannot find an instance") + with e when CErrors.noncritical e -> + let e, info = Exninfo.capture e in + Exninfo.iraise (NotFoundInstance e, info) else ((if debug_ho_unification () then let evi = Evd.find evd evk in |