diff options
| author | Emilio Jesus Gallego Arias | 2018-11-15 04:18:36 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-18 17:17:29 +0100 |
| commit | 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 (patch) | |
| tree | 6131bedbfc1176d14fdf2919913d703e0ba067e1 /lib/flags.mli | |
| parent | 25e989019f72bd435d84a1d495c7de25165556dd (diff) | |
[options] Remove deprecated option automatic introduction.
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index b667235678..e282d4ca8c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -78,9 +78,6 @@ val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit (* Miscellaneus flags for vernac *) -val make_auto_intros : bool -> unit -val is_auto_intros : unit -> bool - val program_mode : bool ref val is_program_mode : unit -> bool |