From 2a805fd99b96746dbfe381d64cd7eaba84fdca79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 10 Jul 2014 15:59:44 +0200
Subject: Feedback: LoadedFile + Goals

LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
---
 proofs/proof_global.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs/proof_global.mli')

diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index d5229c562..2b54b24ef 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -188,3 +188,4 @@ end
 type state
 val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
+val proof_of_state : state -> Proof.proof
-- 
cgit v1.2.3