diff options
| author | Hugo Herbelin | 2015-10-04 08:16:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:05 +0100 |
| commit | 5cdf3cfc8ddfb9854534fadc1a08019e9c472590 (patch) | |
| tree | 5c817c29748b973a2561e418f376f00aa7da3f27 /kernel/declareops.ml | |
| parent | 38e70af82d33de8e977b9b7e347ff501fcd5c2d8 (diff) | |
RefMan, ch. 4: Fixing the definition of terms considered in the section.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions