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')

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