From 945f49236e0db8179548110a056f9787ecffd746 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Jan 2019 10:53:19 +0100
Subject: At Qed, if shelved goals remain, emit a warning instead of an error

This error was more or less a debug tool (checking that no tactic breaks
the invariant). But some users may want to support other models, see
https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
---
 proofs/proof.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'proofs/proof.ml')

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
-- 
cgit v1.2.3