[declare/lemmas] Make inference hook exception-free

This is a step towards cleanup of the `start` lemma path.

2 files changed, 10 insertions, 9 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
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 700ca93c33..abbb745161 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,6 @@ type typing_constraint =
   | OfType of types (** A term of the expected type *)
   | WithoutTypeConstraint (** A term of unknown expected type *)
 
-type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
-
 type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
@@ -103,13 +101,17 @@ val understand_ltac : inference_flags ->
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
 
+(** [hook env sigma ev] returns [Some (sigma', term)] if [ev] can be
+   instantiated with a solution, [None] otherwise. Used to extend
+   [solve_remaining_evars] below. *)
+type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
+
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)
 (* For simplicity, it is assumed that current map has no other evars
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
-
 val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
   env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map