aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-02-14 15:57:49 +0100
committerPierre-Marie Pédrot2015-02-14 16:28:59 +0100
commit150ef1fa8cf93d7aee765cc878287b79b29c787f (patch)
treec56666e3d30f53fbb74e4c3493579eae1953239d /plugins
parentbc77234dc5d40d4540793ceead1595b15ab18bb8 (diff)
Fixing bug #4016.
When setoid rewriting in a hypothesis, we push the newly introduced declaration after the last declaration it depends on.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions