aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/refl_omega.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-18 15:47:50 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-05-22 15:26:59 +0200
commit2561930b8d163507f2a35e1ffddf90a6f14576de (patch)
treeb4d2425c4e11e7263c9dde52cf1ef6090640554a /plugins/romega/refl_omega.ml
parentd992ae9fc539bdadd9214d2c92d83bd08b68ef33 (diff)
ReflOmegaCore: misc cleanup, <? instead of bgt, etc
Diffstat (limited to 'plugins/romega/refl_omega.ml')
0 files changed, 0 insertions, 0 deletions