diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-10 10:31:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-10 10:32:25 +0200 |
| commit | c88f47195955beb615d15dd9d57e4de20e5e3a52 (patch) | |
| tree | 824ebe4739ee767a5c452f32d603510cf14db91a /pretyping/recordops.mli | |
| parent | 7ed370257e576dd084f89eae52fcc2135d4fbee3 (diff) | |
Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions