From b9c6982fb5f60f720fd4c0435414406a9ecca749 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 16:44:27 +0100
Subject: Fixing printing of tactics encapsulated as tacarg with Tacexp.

We preserve the level instead of resetting it at level 0.

Probably it would be the same as giving level ltop since Tacexp
apparently comes only from using a tactic in an Ltac "let", which is
where I observed a problem.
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index ab07e0c242..bc0de0acdf 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1003,7 +1003,7 @@ let pr_goal_selector ~toplevel s =
             | TacAtom (loc,t) ->
               pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
             | TacArg(_,Tacexp e) ->
-              pr.pr_tactic (latom,E) e, latom
+              pr_tac inherited e, latom
             | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
               keyword "constr:" ++ pr.pr_constr c, latom
             | TacArg(_,ConstrMayEval c) ->
-- 
cgit v1.2.3