diff options
| author | Emilio Jesus Gallego Arias | 2018-10-15 14:45:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-15 14:45:09 +0200 |
| commit | b7dae2c97cce2a298bfbbd6f3a72a02e092ebe9e (patch) | |
| tree | 8ee21ee35a2339fa431eb60b3fb04fccaf3f1a64 /kernel/cemitcodes.mli | |
| parent | 68a9b7ceab4af63b5fe7a3bc2d7197dc480fd6d2 (diff) | |
| parent | 7c85593cc820e7480248b9308b95f5808b369191 (diff) | |
Merge PR #8717: Lemmas, DeclareDef: internal reorganization of code highlighting what can be shared
Diffstat (limited to 'kernel/cemitcodes.mli')
0 files changed, 0 insertions, 0 deletions