diff options
| author | Jason Gross | 2018-11-28 15:43:27 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-11-28 15:43:27 -0500 |
| commit | cd85d37a6d40d78592ca6502624b0c70dc84ce56 (patch) | |
| tree | 9989cd135c1522e533c223655710e20c1cc6b376 /dev | |
| parent | 1ca73b4ba5e16af3baed6c804d0d0eeaac9eccd5 (diff) | |
Fix numeral notations doc by indenting
As per https://github.com/coq/coq/pull/8965#discussion_r237225852
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions