diff options
| author | Emilio Jesus Gallego Arias | 2018-03-05 23:38:52 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-10 00:33:08 +0100 |
| commit | 4718f5afec0538781195fdac82ffefb0b7c57535 (patch) | |
| tree | ed60d5b3913f4701ad108e6f9fd007eb3478db24 /dev/include | |
| parent | 123de18a0886233b047ef2bad4bd7b3694f2abcc (diff) | |
[coq] Adapt to coq/coq#6837.
Minor.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions