diff options
| author | Hugo Herbelin | 2014-11-22 18:09:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-22 19:23:32 +0100 |
| commit | b3320b0f942a9f86d5bd1c00876f8816e5c94446 (patch) | |
| tree | 7bb8a6acc55b9711daae22237e55d7c56a05bbab /dev | |
| parent | 250afa5b896a7e8ab5971667e6889ee3a498dfd3 (diff) | |
Attempt to organize and document unification flags of setoid rewrite.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions