aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-07 16:44:27 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-11-15 11:08:25 +0100
commitb9c6982fb5f60f720fd4c0435414406a9ecca749 (patch)
treef211ec79864607cc31f98a17d5d51659d39f8ad2 /plugins/ltac
parent10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 (diff)
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.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/pptactic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index ab07e0c24..bc0de0acd 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) ->