diff options
| author | Pierre-Marie Pédrot | 2016-06-05 21:50:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-15 20:21:37 +0200 |
| commit | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (patch) | |
| tree | 76a95699918b818e3f6111b594b5b6ec7bd566b2 /kernel/declareops.ml | |
| parent | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (diff) | |
Remove the syntax changes introduced by this branch.
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions