diff options
| author | Hugo Herbelin | 2020-08-30 08:14:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 22:34:24 +0200 |
| commit | 561fd5aa45a0643b60637949876401dca6476fe3 (patch) | |
| tree | ab3d76d954c8622773b789cb350a0d0db99d2701 /plugins | |
| parent | 0d11cdd7fe6605666a274168e40acb11e1b05ab6 (diff) | |
Notation.ml: Move interpretation_eq earlier for future use.
Also add optimisation of interpretation_eq.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions