diff options
| author | Lasse Blaauwbroek | 2020-10-22 18:47:23 +0200 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-11-12 21:34:28 +0100 |
| commit | 954f278034c8f95cbc889d1e74230979cde4f70d (patch) | |
| tree | 3f743363ef916ec1118f4111b3f375f9d4570495 /interp/dumpglob.mli | |
| parent | b65e9e9b993930dc5e653a9a1210edcaadbd1537 (diff) | |
Change Dumpglob.pause and Dumpglob.continue into push and pop
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index be1e3f05d2..857991cb3f 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -19,11 +19,19 @@ type glob_output = | MultFiles (* one glob file per .v file *) | File of string (* Single file for all coqc arguments *) -(* Default "NoGlob" *) -val set_glob_output : glob_output -> unit +(** [push_output o] temporarily overrides the output location to [o]. + The original output can be restored using [pop_output] *) +val push_output : glob_output -> unit +(** Restores the original output that was overridden by [push_output] *) +val pop_output : unit -> unit + +(** Alias for [push_output NoGlob] *) val pause : unit -> unit + +(** Deprecated alias for [pop_output] *) val continue : unit -> unit +[@@ocaml.deprecated "Use pop_output"] val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit |