aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/int.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-09 11:20:04 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-11-10 16:38:51 +0100
commitbd1c976531ad6154339fff7e48e85dbe7951de23 (patch)
tree432374009e0a63b7e64a9d75114ccda2173e933d /lib/int.ml
parent2bad1e8d896b40495bc8579e407f142f7f3fb7d9 (diff)
Activating bracketing of last or-and introduction pattern by default
for more regularity.
Diffstat (limited to 'lib/int.ml')
0 files changed, 0 insertions, 0 deletions