diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 16:44:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-15 11:08:25 +0100 |
| commit | b9c6982fb5f60f720fd4c0435414406a9ecca749 (patch) | |
| tree | f211ec79864607cc31f98a17d5d51659d39f8ad2 | |
| parent | 10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 (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.
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
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) -> |