diff options
| author | Maxime Dénès | 2018-10-09 16:45:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-26 13:31:29 +0200 |
| commit | 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 (patch) | |
| tree | b44c6f8bed7e8f4ea09807b1239ab6ee3676aeeb /dev/ci | |
| parent | e2096b9e6048bbab5c6da279bab3c3a719dc237f (diff) | |
Remove a few circumvolutions around parameters of inductive entries
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions