diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 20:35:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 20:35:38 +0200 |
| commit | cf3e5a8e02966c9fe80771c531d9e7d24453733a (patch) | |
| tree | 344e64364a368ac7ccfc2aec25815986aa64a29b /kernel/type_errors.mli | |
| parent | 062e280c283c5cf026004a70f9ab2c1b710ac330 (diff) | |
| parent | d4f034dceb2742459d4cce0d1d74ae9d59106a4d (diff) | |
Merge PR #8545: Functionalize evarmap passing in Cases.ml
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions