From b1af90453f7002dec1994a0be31cfa92659496a8 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 14 Jan 2005 13:06:18 +0000 Subject: Ajout mémorisation numéro commande courante + reset vers ce numéro pour mode emacs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6587 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index c43155816..fa8a34344 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -66,7 +66,8 @@ val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit val mark_end_of_command : unit -> unit - +val current_command_label : unit -> int +val reset_label : int -> unit (*s The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment -- cgit v1.2.3