[proof] Move proofs that have an associated constant to `Lemmas`

The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.

This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.

Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.

As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.

We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.

1 files changed, 33 insertions, 111 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b642e8eea7..f06b2885e2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,65 +36,20 @@ type proof_object = {
 
 type opacity_flag = Opaque | Transparent
 
-type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of opacity_flag *
-              lident option *
-              proof_object
-
-type proof_terminator = proof_ending -> unit
-type closed_proof = proof_object * proof_terminator
-
-type t = {
-  terminator : proof_terminator CEphemeron.key;
-  endline_tactic : Genarg.glob_generic_argument option;
-  section_vars : Constr.named_context option;
-  proof : Proof.t;
-  universe_decl: UState.universe_decl;
-  strength : Decl_kinds.goal_kind;
-}
-
-(* The head of [t] is the actual current proof, the other ones are
-   to be resumed when the current proof is closed or aborted. *)
-type stack = t * t list
-
-let pstate_map f (pf, pfl) = (f pf, List.map f pfl)
-
-let make_terminator f = f
-let apply_terminator f = f
-
-let get_current_pstate (ps,_) = ps
-
-(* combinators for the current_proof lists *)
-let push ~ontop a =
-  match ontop with
-  | None -> a , []
-  | Some (l,ls) -> a, (l :: ls)
-
-let maybe_push ~ontop = function
-  | Some pstate -> Some (push ~ontop pstate)
-  | None -> ontop
+type t =
+  { endline_tactic : Genarg.glob_generic_argument option
+  ; section_vars : Constr.named_context option
+  ; proof : Proof.t
+  ; universe_decl: UState.universe_decl
+  ; strength : Decl_kinds.goal_kind
+  }
 
 (*** Proof Global manipulation ***)
 
-let get_all_proof_names (pf : stack) =
-  let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in
-  pn :: pns
-
-let give_me_the_proof ps = ps.proof
-let get_current_proof_name ps = (Proof.data ps.proof).Proof.name
-let get_current_persistence ps = ps.strength
-
-let with_current_pstate f (ps,psl) =
-  let ps, ret = f ps in
-  (ps, psl), ret
-
-let modify_current_pstate f (ps,psl) =
-  f ps, psl
-
-let modify_proof f ps =
-  let proof = f ps.proof in
-  {ps with proof}
+let get_proof ps = ps.proof
+let get_proof_name ps = (Proof.data ps.proof).Proof.name
+let get_persistence ps = ps.strength
+let modify_proof f p = { p with proof = f p.proof }
 
 let with_proof f ps =
   let et =
@@ -111,13 +66,6 @@ let with_proof f ps =
   let ps = { ps with proof = newpr } in
   ps, ret
 
-let with_current_proof f (ps,rest) =
-  let ps, ret = with_proof f ps in
-  (ps, rest), ret
-
-let simple_with_current_proof f pf =
-  let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
-
 let simple_with_proof f ps =
   let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps
 
@@ -127,21 +75,7 @@ let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf
 let set_endline_tactic tac ps =
   { ps with endline_tactic = Some tac }
 
-let pf_name_eq id ps =
-  let Proof.{ name } = Proof.data ps.proof in
-  Id.equal name id
-
-let discard {CAst.loc;v=id} (ps, psl) =
-  match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with
-  | [] -> None
-  | ps :: psl -> Some (ps, psl)
-
-let discard_current (_, psl) =
-  match psl with
-  | [] -> None
-  | ps :: psl -> Some (ps, psl)
-
-(** [start_proof sigma id pl str goals terminator] starts a proof of name
+(** [start_proof sigma id pl str goals] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
     is (spiwack: for potential printing, I believe is used only by
@@ -149,21 +83,21 @@ let discard_current (_, psl) =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator =
-  { terminator = CEphemeron.create terminator;
-    proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
-    endline_tactic = None;
-    section_vars = None;
-    universe_decl = pl;
-    strength = kind }
-
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
-  { terminator = CEphemeron.create terminator;
-    proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
-    endline_tactic = None;
-    section_vars = None;
-    universe_decl = pl;
-    strength = kind }
+let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals =
+  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+  ; endline_tactic = None
+  ; section_vars = None
+  ; universe_decl = pl
+  ; strength = kind
+  }
+
+let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
+  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+  ; endline_tactic = None
+  ; section_vars = None
+  ; universe_decl = pl
+  ; strength = kind
+  }
 
 let get_used_variables pf = pf.section_vars
 let get_universe_decl pf = pf.universe_decl
@@ -217,7 +151,7 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; terminator; universe_decl; strength } = ps in
+  let { section_vars; proof; universe_decl; strength } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -312,8 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
   { id = name; entries = entries; persistence = strength;
-    universes },
-  fun pr_ending -> CEphemeron.get terminator pr_ending
+    universes }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
@@ -351,22 +284,11 @@ let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
   close_proof ~opaque ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ps)) ps
 
-(** Gets the current terminator without checking that the proof has
-    been completed. Useful for the likes of [Admitted]. *)
-let get_terminator ps = CEphemeron.get ps.terminator
-let set_terminator hook ps =
-  { ps with terminator = CEphemeron.create hook }
-
-let copy_terminators ~src ~tgt =
-  let (ps, psl), (ts,tsl) = src, tgt in
-  assert(List.length psl = List.length tsl);
-  {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
-
 let update_global_env pf =
   let res, () =
   with_proof (fun _ p ->
-     Proof.in_proof p (fun sigma ->
-       let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-       let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in
-         (p, ()))) pf
+        Proof.in_proof p (fun sigma ->
+            let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+            let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in
+            (p, ()))) pf
   in res