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 /kernel/esubst.ml | |
| 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.
Diffstat (limited to 'kernel/esubst.ml')
0 files changed, 0 insertions, 0 deletions