diff options
| author | Pierre-Marie Pédrot | 2018-11-23 14:04:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-23 14:04:25 +0100 |
| commit | f05f4ebe9e91829e2817c63d90ec328f430992c4 (patch) | |
| tree | 631fc42f0e73fc8af5edb5aa77578f82b6edca20 /dev/include | |
| parent | c22494cd30ebfb705530176c322bb42219e2d422 (diff) | |
Fix w.r.t. coq/coq#9051.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions