aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-10-08 16:00:06 +0200
committerMatthieu Sozeau2015-10-08 16:00:41 +0200
commitb6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (patch)
tree1505041402d00c52669f9e430d144c97eae490ff /kernel/cemitcodes.ml
parentdbdef043ea143f871a3710bae36dfc45fd815835 (diff)
Univs: fix bug #3807
Add a flag to disallow minimization to set
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions