1 files changed, 12 insertions, 12 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 1aeb24606b..4ce932b93d 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