diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index dc7ee6a23..e86d1c728 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -242,7 +242,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; |