From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 stm/proofBlockDelimiter.ml | 4 ++--
 stm/stm.ml                 | 7 ++++---
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2ff76e69f8..3d892fa5ca 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,8 +49,8 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.lemmas }) ->
-    Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
-        let proof = Declare.Proof.get_proof proof in
+    Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof ->
+        let proof = Declare.Proof.get 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
diff --git a/stm/stm.ml b/stm/stm.ml
index 943c83ecd3..7aaa359149 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1157,7 +1157,8 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
+    | `Valid (Some vstate) ->
+      Option.map (Vernacstate.LemmaStack.with_top ~f:Declare.Proof.get) vstate.Vernacstate.lemmas
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
@@ -1526,7 +1527,7 @@ end = struct (* {{{ *)
           try
             let _pstate =
               stm_qed_delay_proof ~st ~id:stop
-                ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+                ~proof:pobject ~info:(Declare.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
             ()
           with exn ->
             (* If [stm_qed_delay_proof] fails above we need to use the
@@ -1672,7 +1673,7 @@ end = struct (* {{{ *)
       let proof, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
-      let info = Lemmas.Info.make () in
+      let info = Declare.Info.make () in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
-- 
cgit v1.2.3