aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-09-28 17:49:41 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-09-28 17:49:41 +0200
commited53e048fc5e4b995c1e0c42bf1ba1611c331cce (patch)
treede30a57d59a332cf895724ad6a28d68601f6c51c /lib/flags.mli
parent1c3bc5642fe29855cc4d72aa677ff7ffd4787271 (diff)
Ring_theory: avoid overriding a few notations
Diffstat (limited to 'lib/flags.mli')
0 files changed, 0 insertions, 0 deletions