From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 4 Feb 2020 17:07:34 +0100
Subject: Remove Goptions.opt_name field

The standard use is to repeat the option keywords in lowercase, which
is basically useless.

En passant add doc entry for Dump Arith.
---
 pretyping/typeclasses.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..bcdd02b3ce 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 let get_typeclasses_unique_solutions =
   Goptions.declare_bool_option_and_ref
     ~depr:false
-    ~name:"check that typeclasses proof search returns unique solutions"
     ~key:["Typeclasses";"Unique";"Solutions"]
     ~value:false
 
-- 
cgit v1.2.3