diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:24:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:03:56 +0100 |
| commit | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (patch) | |
| tree | f96740aedb3b99c54afd233e087a29b20a59cae3 /plugins/ltac/pptactic.ml | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Was broken since 8.6.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
0 files changed, 0 insertions, 0 deletions