1 files changed, 16 insertions, 14 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1aeb24606b..e40940f652 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -351,19 +351,13 @@ let dependent_start ~name ~poly goals =
 
 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
 
@@ -375,19 +369,25 @@ let _ = CErrors.register_handler begin function
     | _ -> raise CErrors.Unhandled
   end
 
+let warn_remaining_shelved_goals =
+  CWarnings.create ~name:"remaining-shelved-goals" ~category:"tactics"
+    (fun () -> Pp.str"The proof has remaining shelved goals")
+
+let warn_remaining_unresolved_evars =
+  CWarnings.create ~name:"remaining-unresolved-evars" ~category:"tactics"
+    (fun () -> Pp.str"The proof has unresolved variables")
+
 let return ?pid (p : t) =
   if not (is_done p) then
     raise (OpenProof(pid, UnfinishedProof))
-  else if has_shelved_goals p then
-    raise (OpenProof(pid, HasShelvedGoals))
   else if has_given_up_goals p then
     raise (OpenProof(pid, HasGivenUpGoals))
-  else if has_unresolved_evar p then
-    (* spiwack: for compatibility with <= 8.3 proof engine *)
-    raise (OpenProof(pid, HasUnresolvedEvar))
-  else
+  else begin
+    if has_shelved_goals p then warn_remaining_shelved_goals ()
+    else if has_unresolved_evar p then warn_remaining_unresolved_evars ();
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
+  end
 
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
@@ -415,8 +415,9 @@ let run_tactic env tac pr =
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
   in
+  let { name; poly } = pr in
   let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
-    Proofview.apply env tac sp
+    Proofview.apply ~name ~poly env tac sp
   in
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
@@ -498,7 +499,8 @@ module V82 = struct
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-    let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
+    let { name; poly } = pr in
+    let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g