aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/const_omega.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-15 12:17:14 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:19:13 +0200
commitfdfdbcda1983c229779a09d77ead5033202bfbc7 (patch)
tree6321331282f4cced039c4d31b6a950a44ecd38f6 /plugins/romega/const_omega.mli
parente6eacd35e2822712b35723b372b167ab894d8472 (diff)
romega/const_omega : a few improvements (less try with, no gen equality)
Diffstat (limited to 'plugins/romega/const_omega.mli')
0 files changed, 0 insertions, 0 deletions