From cd9d1d74c8e06184350e9dc6c2cd536c6475616d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 14 Oct 2020 23:53:27 -0700
Subject: For "Typeclasses eauto", search depth should be a natural, not an
 integer

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

(limited to 'plugins')

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..99fd6890e6 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
      set_typeclasses_debug d;
      Option.iter set_typeclasses_strategy s;
      set_typeclasses_depth depth
-- 
cgit v1.2.3