aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/Ncring_initial.v
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 09:41:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 09:41:43 +0200
commit22faf0ba8ca626903ee0f0988953e91252eeab74 (patch)
tree7100610d8bac8a1d44d471d3e70d290a30b960a1 /plugins/setoid_ring/Ncring_initial.v
parent5c12b6833540f1895d1bb198971d3527e70dce8b (diff)
parent73d577c2d959de975415f2807df6a22fa392d335 (diff)
Merge PR #938: [parsing] Remove hacks for reduced Prelude.
Diffstat (limited to 'plugins/setoid_ring/Ncring_initial.v')
0 files changed, 0 insertions, 0 deletions