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.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index ddc8f8482..5079b4b01 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -200,7 +200,6 @@ let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false -let tactic_context_compat = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 -- cgit v1.2.3