From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:07:32 +0200
Subject: Add [_] prefix to unused values which maybe should be kept

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index dc7ee6a234..e86d1c7283 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;
-- 
cgit v1.2.3