diff options
| author | Emilio Jesus Gallego Arias | 2020-03-02 02:01:23 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-19 17:18:54 -0400 |
| commit | eb452f9da5a52df0d74f7a433cfe98e31ab4ab15 (patch) | |
| tree | 41c036ee34347b765d42340c615e303b5e9fe201 /pretyping/pretyping.ml | |
| parent | 0e329b81794c582ca845d2fc547bfdefad89a972 (diff) | |
[declare/lemmas] Make inference hook exception-free
This is a step towards cleanup of the `start` lemma path.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4bab3bd6ea..ded159e484 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -187,7 +187,7 @@ let interp_sort_info ?loc evd l = in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l -type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option type inference_flags = { use_typeclasses : bool; @@ -247,17 +247,16 @@ let apply_typeclasses ~program_mode env sigma frozen fail_evar = else sigma in sigma -let apply_inference_hook hook env sigma frozen = match frozen with +let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with | FrozenId _ -> sigma | FrozenProgress (lazy (_, pending)) -> Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then - try - let sigma, c = hook env sigma evk in + match hook env sigma evk with + | Some (sigma, c) -> Evd.define evk c sigma - with Exit -> - sigma + | None -> sigma else sigma) pending sigma |