diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 10:32:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-13 10:32:57 +0200 |
| commit | 5b932123c05c6ef75333dec4d5b91cce403e935e (patch) | |
| tree | a7b0fa9fc82ffcf43e064b790b7b04a2389ae132 /pretyping/reductionops.ml | |
| parent | 423d3202fa0f244db36a0b1b45edfa61829201e6 (diff) | |
| parent | 5b6aaca42550715300fbd376c2fc0934da554939 (diff) | |
Merge PR#757: Better sectioning on travis log printing in test-suite
Diffstat (limited to 'pretyping/reductionops.ml')
0 files changed, 0 insertions, 0 deletions