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.
---
 doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial/tuto1/src/g_tuto1.mlg')

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 8c2090f3be..dee407bbe4 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -287,7 +287,7 @@ VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
     let sigma, env = Declare.get_current_context pstate in
-    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
+    let pprf = Proof.partial_proof (Declare.Proof.get pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
-- 
cgit v1.2.3


From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:43:01 +0200
Subject: [declare] Reify Proof.t API into the Proof module.

This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
---
 doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/plugin_tutorial/tuto1/src/g_tuto1.mlg')

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index dee407bbe4..d24d968c01 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,7 +286,7 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Declare.get_current_context pstate in
+    let sigma, env = Declare.Proof.get_current_context pstate in
     let pprf = Proof.partial_proof (Declare.Proof.get pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
-- 
cgit v1.2.3