aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tauto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tauto.ml')
-rw-r--r--plugins/ltac/tauto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 561bfc5d7c..19256e054d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -65,7 +65,7 @@ let assoc_flags ist : tauto_flags =
let negation_unfolding = ref true
open Goptions
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optname = "unfolding of not in intuition";