aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2014-05-18 13:03:54 -0400
committerMaxime Dénès2014-05-18 13:03:54 -0400
commite1cf5ccd8df7080d7dd2aadf0305a9d3ba9c5d9d (patch)
treea110112b38c0761030a2395463ddc93e9c0a61a2 /dev
parent1cfec06ce06ae6c783b840a8d59bb89ee34a87ee (diff)
Restored old behavior of injection on proofs by default.
Use Set Injection On Proof to enable the new behavior.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions