diff options
Diffstat (limited to 'plugins/ltac/tauto.ml')
| -rw-r--r-- | plugins/ltac/tauto.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index df186cc46..1e46c253d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -10,7 +10,6 @@ open Term open EConstr open Hipattern open Names -open Pp open Geninterp open Misctypes open Tacexpr @@ -241,7 +240,7 @@ let tauto_uniform_unit_flags = { } (* This is the compatibility mode (not used) *) -let tauto_legacy_flags = { +let _tauto_legacy_flags = { binary_mode = true; binary_mode_bugged_detection = true; strict_in_contravariant_hyp = true; |