[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.

2 files changed, 2 insertions, 2 deletions

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 =