diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-12 10:58:26 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-31 11:27:15 +0200 |
commit | 96bbe0590417d8885ac09abf7d749c12172e16bc (patch) | |
tree | 75e19acb72216ea2784a5464133032638d78dbaf /library/nameops.ml | |
parent | 0e37dc665cf7a6a9ed7d0d10199dd40134cf0148 (diff) |
Tests for new specialize feature + CHANGES.
Diffstat (limited to 'library/nameops.ml')
0 files changed, 0 insertions, 0 deletions