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.

3 files changed, 19 insertions, 17 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
diff --git a/proofs/proof.mli b/proofs/proof.mli
index fd5e905a3b..40e8ff7eef 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -130,13 +130,10 @@ val compact : t -> t
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
     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. *)
+    Raises [HasGivenUpGoals] if some goals have been given up. *)
 type open_error_reason =
   | UnfinishedProof
-  | HasShelvedGoals
   | HasGivenUpGoals
-  | HasUnresolvedEvar
 
 exception OpenProof of Names.Id.t option * open_error_reason
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f8adc58921..4cc73f419e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -443,8 +443,13 @@ let return_proof ?(allow_partial=false) () =
   (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
      side-effects... This may explain why one need to uniquize side-effects
      thereafter... *)
+  let proof_opt c =
+    match EConstr.to_constr_opt evd c with
+    | Some p -> p
+    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  in
   let proofs =
-    List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
+    List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~opaque ~feedback_id proof =