aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorPierre Letouzey2016-09-28 17:49:41 +0200
committerPierre Letouzey2016-09-28 17:49:41 +0200
commited53e048fc5e4b995c1e0c42bf1ba1611c331cce (patch)
treede30a57d59a332cf895724ad6a28d68601f6c51c /kernel/type_errors.mli
parent1c3bc5642fe29855cc4d72aa677ff7ffd4787271 (diff)
Ring_theory: avoid overriding a few notations
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions