aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-22 10:44:51 +0200
committerPierre-Marie Pédrot2020-10-21 12:19:02 +0200
commit2b91a8989687e152f7120aa6c907ffeba8495bab (patch)
tree0fd0362eccc5c894b08c65147f0229fcdc8d2814 /interp/notation_ops.ml
parent8f16b1c5b97411b7ea88279699f0f410f1c77723 (diff)
Deprecate the non-qualified equality functions on kerpairs.
This allows to quickly spot the parts of the code that rely on the canonical ordering. When possible we directly introduce the quotient-aware versions.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions