diff options
Diffstat (limited to 'toplevel/vernacentries.mli')
| -rw-r--r-- | toplevel/vernacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 0f793bbb9..9fbe7574c 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -18,4 +18,4 @@ val show_open_subgoals : unit -> unit val show_nth_open_subgoal : int -> unit val show_open_subgoals_focused : unit -> unit val show_node : unit -> unit -val print_loadpath : unit -> unit + |