[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.

2 files changed, 14 insertions, 17 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index dfa681395a..7ff6ed9dfb 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -48,15 +48,14 @@ let simple_goal sigma g gs =
 let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
-  | `Valid (Some { Vernacstate.proof }) ->
-    Option.cata (fun proof ->
-        let proof = Proof_global.get_current_pstate proof in
-        let proof = Proof_global.give_me_the_proof proof in
+  | `Valid (Some { Vernacstate.lemmas }) ->
+    Option.cata (Lemmas.Stack.with_top_pstate ~f:(fun proof ->
+        let proof = Proof_global.get_proof proof in
         let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
         let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
         if List.for_all (fun x -> simple_goal sigma x rest) focused
         then `Simple focused
-        else `Not) `Not proof
+        else `Not)) `Not lemmas
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 5baa6ce251..a282efe265 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -881,7 +881,7 @@ end = struct (* {{{ *)
   let invalidate_cur_state () = cur_id := Stateid.dummy
 
   type proof_part =
-    Proof_global.stack option *
+    Lemmas.Stack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
     Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
@@ -890,9 +890,9 @@ end = struct (* {{{ *)
     [ `Full of Vernacstate.t
     | `ProofOnly of Stateid.t * proof_part ]
 
-  let proof_part_of_frozen { Vernacstate.proof; system } =
+  let proof_part_of_frozen { Vernacstate.lemmas; system } =
     let st = States.summary_of_state system in
-    proof,
+    lemmas,
     Summary.project_from_summary st Util.(pi1 summary_pstate),
     Summary.project_from_summary st Util.(pi2 summary_pstate),
     Summary.project_from_summary st Util.(pi3 summary_pstate)
@@ -956,17 +956,17 @@ end = struct (* {{{ *)
            try
             let prev = (VCS.visit id).next in
             if is_cached_and_valid prev
-            then { s with proof =
+            then { s with lemmas =
                 PG_compat.copy_terminators
-                  ~src:((get_cached prev).proof) ~tgt:s.proof }
+                  ~src:((get_cached prev).lemmas) ~tgt:s.lemmas }
             else s
            with VCS.Expired -> s in
          VCS.set_state id (FullState s)
     | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
          if is_cached_and_valid ontop then
            let s = get_cached ontop in
-           let s = { s with proof =
-             PG_compat.copy_terminators ~src:s.proof ~tgt:pstate } in
+           let s = { s with lemmas =
+             PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
                begin
@@ -1168,9 +1168,7 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) ->
-      Option.map (fun p -> Proof_global.(give_me_the_proof (get_current_pstate p)))
-        vstate.Vernacstate.proof
+    | `Valid (Some vstate) -> Option.map (Lemmas.Stack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
@@ -2310,8 +2308,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
              Proofview.give_up else Proofview.tclUNIT ()
               end in
            match (VCS.get_info base_state).state with
-           | FullState { Vernacstate.proof } ->
-               Option.iter PG_compat.unfreeze proof;
+           | FullState { Vernacstate.lemmas } ->
+               Option.iter PG_compat.unfreeze lemmas;
                PG_compat.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
                  fst (Pfedit.solve Goal_select.SelectAll None tac p), ());