From 177f7fa97dc7a2c4459f1a1047dec801ff0c65c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Nov 2018 04:18:36 +0100
Subject: [options] Remove deprecated option automatic introduction.

---
 lib/flags.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'lib/flags.mli')

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
 
-- 
cgit v1.2.3