[proof] Split return_proof in partial and regular versions.

This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.

5 files changed, 49 insertions, 46 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ba8eba0eed..c1156b9afe 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1501,7 +1501,7 @@ end = struct (* {{{ *)
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      let p = PG_compat.return_proof ~allow_partial:drop_pt () in
+      let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in
       if drop_pt then feedback ~id Complete;
       p)
 
@@ -1661,7 +1661,7 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
       if drop then
-        let _proof = PG_compat.return_proof ~allow_partial:true () in
+        let _proof = PG_compat.return_partial_proof () in
         `OK_ADMITTED
       else begin
       let opaque = Proof_global.Opaque in
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 8d62d1635d..8597d1ab09 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -141,8 +141,35 @@ let private_poly_univs =
   in
   fun () -> !b
 
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
-                ((elist, uctx) : closed_proof_output) ps =
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+let return_proof { proof } =
+  let Proof.{name=pid;entry} = Proof.data proof in
+  let initial_goals = Proofview.initial_goals entry in
+  let evd = Proof.return ~pid proof in
+  let eff = Evd.eval_side_effects evd in
+  let evd = Evd.minimize_universes evd in
+  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
+  (* 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... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
+  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+  let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
+  proofs, Evd.evar_universe_context evd
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+  let elist, uctx = return_proof ps in
   let { section_vars; proof; udecl; initial_euctx } = ps in
   let Proof.{ name; poly; entry; sigma } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
@@ -200,7 +227,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
   let entry_fn p (_, t) =
     let t = EConstr.Unsafe.to_constr t in
     let (typ, univs), ((body,univc),eff) = make_body t p in
-    Declare.definition_entry ~opaque ?feedback_id ?section_vars ~univs ~univc ~types:typ ~eff body
+    Declare.definition_entry ~opaque ?section_vars ~univs ~univc ~types:typ ~eff body
   in
   let entries = CList.map2 entry_fn elist (Proofview.initial_goals entry) in
   { name; entries; uctx }
@@ -254,48 +281,19 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
   let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
   { name; entries; uctx }
 
-let return_proof ?(allow_partial=false) ps =
- let { proof } = ps in
- if allow_partial then begin
-  let proofs = Proof.partial_proof proof in
-  let Proof.{sigma=evd} = Proof.data proof in
-  let eff = Evd.eval_side_effects evd in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+let return_partial_proof { proof } =
+ let proofs = Proof.partial_proof proof in
+ let Proof.{sigma=evd} = Proof.data proof in
+ let eff = Evd.eval_side_effects evd in
+ (* 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 proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
-    proofs, Evd.evar_universe_context evd
- end else
-  let Proof.{name=pid;entry} = Proof.data proof in
-  let initial_goals = Proofview.initial_goals entry in
-  let evd = Proof.return ~pid proof in
-  let eff = Evd.eval_side_effects evd in
-  let evd = Evd.minimize_universes evd in
-  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
-  (* 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... *)
-  (* EJGA: actually side-effects de-duplication and this codepath is
-     unrelated. Duplicated side-effects arise from incorrect scheme
-     generation code, the main bulk of it was mostly fixed by #9836
-     but duplication can still happen because of rewriting schemes I
-     think; however the code below is mostly untested, the only
-     code-paths that generate several proof entries are derive and
-     equations and so far there is no code in the CI that will
-     actually call those and do a side-effect, TTBOMK *)
-  let proofs =
-    List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
-    proofs, Evd.evar_universe_context evd
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~opaque ~feedback_id ps proof =
   close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps
 
-let close_proof ~opaque ~keep_body_ucst_separate ps =
-  close_proof ~opaque ~keep_body_ucst_separate (return_proof ps) ps
 
 let update_global_env =
   map_proof (fun p ->
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 44b78ee911..339a7f1898 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -75,9 +75,12 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> pr
 
 type closed_proof_output
 
-(* If allow_partial is set (default no) then an incomplete proof
- * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> t -> closed_proof_output
+(** Requires a complete proof. *)
+val return_proof : t -> closed_proof_output
+
+(** An incomplete proof is allowed (no error), and a warn is given if
+   the proof is complete. *)
+val return_partial_proof : t -> closed_proof_output
 val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
   closed_proof_output Future.computation -> proof_object
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 7c191a1f86..b722acd1ad 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -164,7 +164,8 @@ module Proof_global = struct
   type closed_proof = Proof_global.proof_object * Lemmas.Info.t
 
 
-  let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
+  let return_proof () = cc return_proof
+  let return_partial_proof () = cc return_partial_proof
 
   let close_future_proof ~opaque ~feedback_id pf =
     cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 2c9c7ecc6f..b6b24c9275 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -65,7 +65,8 @@ module Proof_global : sig
   val with_current_proof :
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
-  val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
+  val return_proof : unit -> Proof_global.closed_proof_output
+  val return_partial_proof : unit -> Proof_global.closed_proof_output
 
   type closed_proof = Proof_global.proof_object * Lemmas.Info.t