diff options
| author | Hugo Herbelin | 2016-04-13 21:17:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:43:28 +0200 |
| commit | 0d79eb707cf56c66a169c0f9b368d005bfec4efa (patch) | |
| tree | 41e8c56310658b1d381c58bd147d88cd838b7089 /plugins | |
| parent | 411a0c9b05a73d6081f47b0f0f7aa2c859393b76 (diff) | |
Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.
No other changes (long only because of a change of indentation).
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions