diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-14 15:57:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-14 16:28:59 +0100 |
| commit | 150ef1fa8cf93d7aee765cc878287b79b29c787f (patch) | |
| tree | c56666e3d30f53fbb74e4c3493579eae1953239d /pretyping/typeclasses_errors.mli | |
| parent | bc77234dc5d40d4540793ceead1595b15ab18bb8 (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 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions