diff options
| author | herbelin | 2013-05-05 22:47:35 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-05 22:47:35 +0000 |
| commit | df313cefbaddb57f89650171e59e3abcb168a273 (patch) | |
| tree | d454b60baf938da9a3c2a59e70fc474750057b0f /lib/flags.mli | |
| parent | 9b67b88dc13cbd0720cf88e105a60732f8ab619b (diff) | |
Now printing body of abbreviations (i.e. notation with a name) with
full usage of notations instead of the previous cheap way to prevent
circularity in printing by deactivating all notations.
(Since "->" became a notation, printing abbreviations without
notations at all had become even more inconvenient).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 8ff9deeaae..3965713fe2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -60,13 +60,16 @@ val is_program_mode : unit -> bool val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit -(** Temporary activate an option (to activate option [o] on [f x y z], +(** Temporarily activate an option (to activate option [o] on [f x y z], use [with_option o (f x y) z]) *) val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b -(** Temporary deactivate an option *) +(** Temporarily deactivate an option *) val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b +(** Temporarily extends the reference to a list *) +val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b + (** If [None], no limit *) val set_print_hyps_limit : int option -> unit val print_hyps_limit : unit -> int option |