aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega/coq_omega.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-17 13:39:59 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:26:59 +0200
commit7509f5c8eab84fda5a9029329c6b70758259765f (patch)
tree64b2d9b007f2a09ea3e2d1dcec8a774d54437427 /plugins/omega/coq_omega.ml
parenteae11e85b5fe578fbec404b91628062aa255be92 (diff)
ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT
Diffstat (limited to 'plugins/omega/coq_omega.ml')
0 files changed, 0 insertions, 0 deletions