aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-16 11:11:51 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-16 11:11:51 +0200
commitc122e1827aae252716da56ab46eeed4046c4aefc (patch)
treede16215c11580a284b9c539c93e381efdcecf6f7 /plugins/setoid_ring
parent768883a6b7002bcdc589b43c199b2c0b1d2c23b5 (diff)
[ssr] fix after to_constr ~abort_on_undefined_evars was added
Diffstat (limited to 'plugins/setoid_ring')
0 files changed, 0 insertions, 0 deletions