From 487a91d8e44df95c0e18595c5463c5acfeee3174 Mon Sep 17 00:00:00 2001
From: bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 8 Feb 2001 07:46:13 +0000
Subject: exporting traverse_to and mutate: they are used in pcoq.

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

(limited to 'proofs')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8b8e41b34..128c2b265 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -143,3 +143,9 @@ val traverse : int -> unit
 val traverse_nth_goal : int -> unit
 val traverse_next_unproven : unit -> unit
 val traverse_prev_unproven : unit -> unit
+
+
+(* These two functions make it possible to implement more elaborate
+   proof and goal management, as it is done, for instance in pcoq *)
+val traverse_to : int list -> unit
+val mutate : (pftreestate -> pftreestate) -> unit
-- 
cgit v1.2.3