diff options
| author | Arnaud Spiwack | 2015-10-29 20:52:32 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-10-29 20:52:32 +0100 |
| commit | 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 (patch) | |
| tree | 8284dc3eda6ddb7db3e3bd6a5e262d1bb2934868 /interp/notation.ml | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
Make the code of compare functions linear in the number of constructors.
This scheme has been advised by @gashe on #79.
Interestingly there are several comparison functions in Coq which were already implemented with this scheme.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions