[declare/lemmas] Make inference hook exception-free

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

3 files changed, 18 insertions, 14 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
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e7930cc091..30a1475e60 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -473,11 +473,14 @@ let program_inference_hook env sigma ev =
     let concl = evi.Evd.evar_concl in
     if not (Evarutil.is_ground_env sigma env &&
             Evarutil.is_ground_term sigma concl)
-    then raise Exit;
-    let c, _, _, ctx =
-      Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
-    in Evd.set_universe_context sigma ctx, EConstr.of_constr c
-  with Logic_monad.TacticFailure e when noncritical e ->
+    then None
+    else
+      let c, _, _, ctx =
+        Pfedit.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
+      in
+      Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
+  with
+  | Logic_monad.TacticFailure e when noncritical e ->
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")