From 70f67f4d30269170faca5131b3a3c348822d6dd6 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Thu, 1 Mar 2012 16:28:44 +0000
Subject: Removed a superfluous function in proof.mli. Preparing for incoming
 changes of the handling of unfocusing errors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15010 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof.mli | 2 --
 1 file changed, 2 deletions(-)

diff --git a/proofs/proof.mli b/proofs/proof.mli
index 15ee7cf06d..ae3430535d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -127,8 +127,6 @@ val no_focused_goal : proof -> bool
 
 val get_proof_info : proof -> Store.t
 
-val set_proof_info : Store.t -> proof -> unit
-
 (* Sets the section variables assumed by the proof *)
 val set_used_variables : Sign.section_context -> proof -> unit
 val get_used_variables : proof -> Sign.section_context option
-- 
cgit v1.2.3