diff options
Diffstat (limited to 'toplevel/mltop.mli')
| -rw-r--r-- | toplevel/mltop.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 715355635..2b5de5708 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -8,9 +8,9 @@ (*i $Id$ i*) -(* If there is a toplevel under Coq, it is described by the following +(* If there is a toplevel under Coq, it is described by the following record. *) -type toplevel = { +type toplevel = { load_obj : string -> unit; use_file : string -> unit; add_dir : string -> unit; |