From ac2b757a7835672ba494bf42244b5d393e8db089 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 7 Dec 2017 22:27:19 +0100 Subject: Remove deprecated option Tactic Compat Context. And some code simplification. --- lib/flags.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'lib/flags.mli') diff --git a/lib/flags.mli b/lib/flags.mli index c4afb8318..8825390e6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -160,10 +160,6 @@ val native_compiler : bool ref (** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref -val tactic_context_compat : bool ref -(** Set to [true] to trigger the compatibility bugged context matching (old - context vs. appcontext) is set. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref -- cgit v1.2.3