diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/discharge.ml | 6 | ||||
| -rw-r--r-- | library/discharge.mli | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/library/discharge.ml b/library/discharge.ml new file mode 100644 index 0000000000..17a70b2095 --- /dev/null +++ b/library/discharge.ml @@ -0,0 +1,6 @@ + +(* $Id$ *) + +open Declare + +let close_section _ s = Lib.close_section s diff --git a/library/discharge.mli b/library/discharge.mli index 7b22e2eade..34b8bd1c7f 100644 --- a/library/discharge.mli +++ b/library/discharge.mli @@ -1,4 +1,4 @@ (* $Id$ *) -val close_section : string -> unit +val close_section : bool -> string -> unit |