From 1559f734060e49fe09d7221f63dd66e8e7d565a4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Oct 2016 20:17:48 +0200 Subject: Tests for info/debug auto/eauto. This is while waiting for a deeper uniformization of auto, eauto, and typeclasses eauto. Incidentally includes a little fix in harmonizing auto/eauto printing. --- tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index d4251555d..7558a707e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -259,7 +259,7 @@ and erase_subtree depth = function | (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l let pr_info_atom (d,pp) = - str (String.make d ' ') ++ pp () ++ str "." + str (String.make (d-1) ' ') ++ pp () ++ str "." let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> -- cgit v1.2.3