diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 20:51:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 20:51:40 +0200 |
| commit | f96dc97f48df5d0fdf252be5f28478a58be77961 (patch) | |
| tree | 5d741e02de71083b5e279121721dff7cb4b56516 /proofs/redexpr.ml | |
| parent | 17f68d403d248e899efbb76afeed169232946ecf (diff) | |
Fix bug #3593, making constr_eq and progress work up to
equality of universes, along with a few other functions in evd.
Diffstat (limited to 'proofs/redexpr.ml')
0 files changed, 0 insertions, 0 deletions