From 99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 21 Nov 2018 19:18:48 +0100
Subject: Goptions.declare_* functions return unit instead of a write_function

Returning a writer insinuates that it is not exactly the same as the
writer which was passed as argument, but that is incorrect.
---
 tactics/class_tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 5959dd54b1..b349accbc9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -113,7 +113,7 @@ let _ =
       optread  = get_typeclasses_filtered_unification;
       optwrite = set_typeclasses_filtered_unification; }
 
-let set_typeclasses_debug =
+let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "debug output for typeclasses proof search";
@@ -137,7 +137,7 @@ let _ =
       optread  = get_typeclasses_verbose;
       optwrite = set_typeclasses_verbose; }
 
-let set_typeclasses_depth =
+let _ =
   declare_int_option
     { optdepr  = false;
       optname  = "depth for typeclasses proof search";
-- 
cgit v1.2.3