aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/refl_omega.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 13:31:54 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 13:41:16 +0100
commit1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 (patch)
tree15aadd829fe3e8c3ee0a747de34a9b96614bfdba /plugins/romega/refl_omega.ml
parent968dfdb15cc11d48783017b2a91147b25c854ad6 (diff)
Renaming functions in Typing to stick to the standard e_* scheme.
Diffstat (limited to 'plugins/romega/refl_omega.ml')
0 files changed, 0 insertions, 0 deletions