diff options
-rw-r--r-- | tactics/class_tactics.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 95b26c2d5..0172d28c5 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -851,6 +851,15 @@ let set_typeclasses_debug = optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } +let set_typeclasses_debug = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "debug output for typeclasses proof search"; + optkey = ["Debug";"Typeclasses"]; + optread = get_typeclasses_debug; + optwrite = set_typeclasses_debug; } + let set_typeclasses_depth = declare_int_option { optsync = true; |