[proof] Provide better control of "open proofs" exceptions.

This is inspired and an alternative to #8981. We consolidate the "open
proof" exception, allowing clients to explicitly capture it and
removing some ugly duplicated code in the way.

The `Solve Obligation tac` semantics are then tweaked as to removed
the wide-scope "catch-all" and indeed will now relay errors in `tac`
as it will only absorb tactics that don't error but fail to close the
goal such as `auto`. For the rest of the cases, we introduce a
warning, and may move to a full error in later releases.

We also remove an unnecessary `tclCOMPLETE` call to code that will
actually call `close_proof`. In this case, it is better to delegate
error management to the core function.

Some error messages have changed [as we consolidate two error paths]
so this PR may require adjustment in that area.

9 files changed, 99 insertions, 86 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4d5711c195..f9e2edd888 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,8 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Proof.OpenProof _
+  (* abstract will call close_proof inside a tactic *)
   | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8220949856..76a9a9f4c8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -335,28 +335,42 @@ let dependent_start goals =
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
+type open_error_reason =
+  | UnfinishedProof
+  | HasShelvedGoals
+  | HasGivenUpGoals
+  | HasUnresolvedEvar
+
+let print_open_error_reason er = let open Pp in match er with
+  | UnfinishedProof ->
+    str "Attempt to save an incomplete proof"
+  | HasShelvedGoals ->
+    str "Attempt to save a proof with shelved goals"
+  | HasGivenUpGoals ->
+    strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed."
+  | HasUnresolvedEvar ->
+    strbrk "Attempt to save a proof with existential variables still non-instantiated"
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
 let _ = CErrors.register_handler begin function
-  | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
-  | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
-  | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
-  | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
-  | _ -> raise CErrors.Unhandled
-end
+    | OpenProof (pid, reason) ->
+      let open Pp in
+      Option.cata (fun pid ->
+          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason
+    | _ -> raise CErrors.Unhandled
+  end
 
-let return p =
+let return ?pid (p : t) =
   if not (is_done p) then
-    raise UnfinishedProof
+    raise (OpenProof(pid, UnfinishedProof))
   else if has_shelved_goals p then
-    raise HasShelvedGoals
+    raise (OpenProof(pid, HasShelvedGoals))
   else if has_given_up_goals p then
-    raise HasGivenUpGoals
+    raise (OpenProof(pid, HasGivenUpGoals))
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
-    raise HasUnresolvedEvar
+    raise (OpenProof(pid, HasUnresolvedEvar))
   else
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
@@ -449,11 +463,10 @@ module V82 = struct
 
   let grab_evars p =
     if not (is_done p) then
-      raise UnfinishedProof
+      raise (OpenProof(None, UnfinishedProof))
     else
       { p with proofview = Proofview.V82.grab p.proofview }
 
-
   (* Main component of vernac command Existential *)
   let instantiate_evar n com pr =
     let tac =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 8cf543557b..aaabea3454 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -89,11 +89,15 @@ val compact : t -> t
     Raises [HasShelvedGoals] if some goals are left on the shelf.
     Raises [HasGivenUpGoals] if some goals have been given up.
     Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
-val return : t -> Evd.evar_map
+type open_error_reason =
+  | UnfinishedProof
+  | HasShelvedGoals
+  | HasGivenUpGoals
+  | HasUnresolvedEvar
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
+val return : ?pid:Names.Id.t -> t -> Evd.evar_map
 
 (*** Focusing actions ***)
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 25cf789193..cb4b5759dc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -176,7 +176,6 @@ let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
 let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
 
-
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
   match !pstates with
@@ -416,20 +415,7 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
-  let evd =
-    let error s =
-      let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
-    in
-    try Proof.return proof with
-    | Proof.UnfinishedProof ->
-        error(str"Attempt to save an incomplete proof")
-    | Proof.HasShelvedGoals ->
-        error(str"Attempt to save a proof with shelved goals")
-    | Proof.HasGivenUpGoals ->
-        error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.")
-    | Proof.HasUnresolvedEvar->
-        error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
+  let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 197f71ca91..f9bb2c3d60 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,9 +2,9 @@ Miscprint
 Goal
 Evar_refiner
 Proof_type
-Logic
 Refine
 Proof
+Logic
 Goal_select
 Proof_bullet
 Proof_global
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 81cf9289d1..328e3df5ad 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -358,7 +358,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
     Eauto.registered_e_assumption ::
     (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve])
   in
-  tclFIRST (List.map tclCOMPLETE tacl)
+  tclSOLVE tacl
 
 and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl =
   let open Proofview.Notations in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 5067315d08..c141fdba31 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -151,7 +151,7 @@ let rec e_trivial_fail_db db_list local_db =
     (Tacticals.New.tclTHEN Tactics.intro next) ::
     (List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
-  Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
+  Tacticals.New.tclSOLVE tacl
   end
 
 and e_my_find_search env sigma db_list local_db secvars hdc concl =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c2805674e4..b1deee7798 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -826,18 +826,34 @@ let rec string_of_list sep f = function
   | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
+let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err ->
+    Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl ();
+            str "This will become an error in the future"])
 
-let solve_by_tac name evi t poly ctx =
+let solve_by_tac ?loc name evi t poly ctx =
   let id = name in
   (* spiwack: the status is dropped. *)
-  let (entry,_,ctx') = Pfedit.build_constant_by_tactic
-    id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
-  let env = Global.env () in
-  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
-  let body, () = Future.force entry.const_entry_body in
-  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
-  Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
-  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'
+  try
+    let (entry,_,ctx') =
+      Pfedit.build_constant_by_tactic
+        id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
+    let env = Global.env () in
+    let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
+    let body, () = Future.force entry.const_entry_body in
+    let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
+    Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
+    Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
+  with
+  | Refiner.FailError (_, s) as exn ->
+    let _ = CErrors.push exn in
+    user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
+  (* If the proof is open we absorb the error and leave the obligation open *)
+  | Proof.OpenProof _ ->
+    None
+  | e when CErrors.noncritical e ->
+    let err = CErrors.print e in
+    warn_solve_errored ?loc err;
+    None
 
 let obligation_terminator name num guard hook auto pf =
   let open Proof_global in
@@ -987,41 +1003,34 @@ and solve_obligation_by_tac prg obls i tac =
     match obl.obl_body with
     | Some _ -> None
     | None ->
-	try
-	  if List.is_empty (deps_remaining obls obl.obl_deps) then
-	    let obl = subst_deps_obl obls obl in
-	    let tac =
-	      match tac with
-	      | Some t -> t
-	      | None ->
-		  match obl.obl_tac with
-		  | Some t -> t
-		  | None -> !default_tactic
-	    in
-	    let evd = Evd.from_ctx prg.prg_ctx in
-	    let evd = Evd.update_sigma_env evd (Global.env ()) in
-	    let t, ty, ctx =
-              solve_by_tac obl.obl_name (evar_of_obligation obl) tac
-                (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
-            in
-            let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
-            let prg = {prg with prg_ctx = ctx} in
-            let def, obl' = declare_obligation prg obl t ty uctx in
-              obls.(i) <- obl';
-	      if def && not (pi2 prg.prg_kind) then (
-	        (* Declare the term constraints with the first obligation only *)
-	        let evd = Evd.from_env (Global.env ()) in
-	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
-		let ctx' = Evd.evar_universe_context evd in
-		  Some {prg with prg_ctx = ctx'})
-	      else Some prg
-	  else None
-	with e when CErrors.noncritical e ->
-          let (e, _) = CErrors.push e in
-          match e with
-	  | Refiner.FailError (_, s) ->
-	      user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s)
-          | e -> None (* FIXME really ? *)
+      if List.is_empty (deps_remaining obls obl.obl_deps) then
+        let obl = subst_deps_obl obls obl in
+        let tac =
+          match tac with
+          | Some t -> t
+          | None ->
+            match obl.obl_tac with
+            | Some t -> t
+            | None -> !default_tactic
+        in
+        let evd = Evd.from_ctx prg.prg_ctx in
+        let evd = Evd.update_sigma_env evd (Global.env ()) in
+        match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
+                (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with
+        | None -> None
+        | Some (t, ty, ctx) ->
+          let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+          let prg = {prg with prg_ctx = ctx} in
+          let def, obl' = declare_obligation prg obl t ty uctx in
+          obls.(i) <- obl';
+          if def && not (pi2 prg.prg_kind) then (
+            (* Declare the term constraints with the first obligation only *)
+            let evd = Evd.from_env (Global.env ()) in
+            let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
+            let ctx' = Evd.evar_universe_context evd in
+            Some {prg with prg_ctx = ctx'})
+          else Some prg
+      else None
 
 and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1fab35b650..7b81fbf81b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -457,8 +457,7 @@ let start_proof_and_print k l hook =
                   Evarutil.is_ground_term sigma concl)
           then raise Exit;
           let c, _, ctx =
-            Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
-                                   concl (Tacticals.New.tclCOMPLETE tac)
+            Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac
           in Evd.set_universe_context sigma ctx, EConstr.of_constr c
         with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
           user_err Pp.(str "The statement obligations could not be resolved \