aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-19 21:24:55 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-19 21:25:59 +0200
commit8bd3e4eba54ace61f49a53b8ce74517de71006ec (patch)
tree4ca4c75f1628e7500aae6d7d129eb9df72191f9d /plugins/omega
parent234dc568769602cb91655929a344027a15f52845 (diff)
Exporting some functions of vars.ml as functions operating on EConstr.
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions