diff options
| author | herbelin | 2003-10-13 08:55:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-13 08:55:34 +0000 |
| commit | e3decbc5b56877a48463fef41fd65b4e4ec0ec61 (patch) | |
| tree | 7e237f7e3570563644c5b2ab6d716b6d538eafd9 | |
| parent | 97569cb0dbe0abe2303a85f8f97f7d666b649320 (diff) | |
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
| -rw-r--r-- | toplevel/vernacentries.mli | 17 |
1 files changed, 1 insertions, 16 deletions
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 |