From c8ca50f0cf961c9e31489f095463a99fc005c5de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Sep 2016 00:06:16 +0200
Subject: Fix bug #5093: typeclasses eauto depth arg does not accept a var.

---
 ltac/g_class.ml4 | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'ltac')

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index eaa6aad4f6..18df596eb8 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
-let pr_depth _prc _prlc _prt = function
-    Some i -> Pp.int i
-  | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
-  | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
      set_typeclasses_debug d;
      set_typeclasses_depth depth
    ]
@@ -63,9 +55,9 @@ END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     [ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
      typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
 
-- 
cgit v1.2.3