From 13738c4afd217ea7d71e654c38fc6a661bd2953c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 24 Oct 2016 13:38:07 +0200
Subject: Fix printing of typeclasses eauto debug wrt intro.

---
 tactics/class_tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0944cbe38f..248635b4e4 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1141,7 +1141,8 @@ module Search = struct
                        (true,false,false) info.search_only_classes None decl in
     let ldb = Hint_db.add_list env s hint info.search_hints in
     let info' =
-      { info with search_hints = ldb; last_tac = lazy (str"intro") }
+      { info with search_hints = ldb; last_tac = lazy (str"intro");
+        search_depth = 1 :: 1 :: info.search_depth }
     in kont info'
 
   let intro info kont =
-- 
cgit v1.2.3