From 2a805fd99b96746dbfe381d64cd7eaba84fdca79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
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.ml  | 1 +
 proofs/proof_global.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 06afc2fa9a..7c7ff0c940 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -515,4 +515,5 @@ let freeze ~marshallable =
   | `Shallow -> !pstates
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
+let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index d5229c5625..2b54b24ef2 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