Merge PR #9347: At Qed, if shelved goals remain, emit a warning instead of an error

Ack-by: maximedenes
Reviewed-by: ppedrot

6 files changed, 30 insertions, 17 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6532e08e9d..49cbc4d7e5 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
     For getting the evar-normal form of a term with evars see
    {!Evarutil.nf_evar}. *)
 
+val to_constr_opt : Evd.evar_map -> t -> Constr.t option
+(** Same as [to_constr], but returns [None] if some unresolved evars remain *)
+
 val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 31c326df6a..eee2cb700c 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1376,6 +1376,13 @@ module MiniEConstr = struct
     in
     UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
 
+  let to_constr_opt sigma c =
+    let evar_value ev = Some (existential_value sigma ev) in
+    try
+      Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c)
+    with NotInstantiatedEvar ->
+      None
+
   let of_named_decl d = d
   let unsafe_to_named_decl d = d
   let of_rel_decl d = d
diff --git a/engine/evd.mli b/engine/evd.mli
index 7560d68805..de73144895 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -689,6 +689,7 @@ module MiniEConstr : sig
   val of_constr_array : Constr.t array -> t array
 
   val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
+  val to_constr_opt : evar_map -> t -> Constr.t option
 
   val unsafe_to_constr : t -> Constr.t
   val unsafe_to_constr_array : t array -> Constr.t array
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 =