From e3decbc5b56877a48463fef41fd65b4e4ec0ec61 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 08:55:34 +0000
Subject: Deplacement pr_subgoal and co vers Pfedit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4609 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.mli | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 2e6e35df4f..1a9bf9b1d2 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -16,25 +16,10 @@ open Vernacexpr
 open Topconstr
 (*i*)
 
-(* Vernacular entries. This module registers almost all the vernacular entries,
-   by side-effects using [Vernacinterp.vinterp_add]. *)
-
-(* Moved to g_vernac.ml4
-val join_binders : ('a list * 'b) list -> ('a * 'b) list
-*)
-
-(* Synonym for Vernacinterp.vinterp_add
-val add : string -> (Vernacexpr.vernac_arg list -> unit -> unit) -> unit
-*)
+(* Vernacular entries *)
 
 val show_script : unit -> unit
 val show_prooftree : unit -> unit
-val show_open_subgoals : unit -> unit
-val show_nth_open_subgoal : int -> unit
-
-(* Merged with show_open_subgoals !
-val show_open_subgoals_focused : unit -> unit
-*)
 
 val show_node : unit -> unit
 
-- 
cgit v1.2.3