diff options
| author | Emilio Jesus Gallego Arias | 2018-03-05 22:10:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-10 00:32:50 +0100 |
| commit | 123de18a0886233b047ef2bad4bd7b3694f2abcc (patch) | |
| tree | 372ec9a7e74c3b1ea1a2cd834cc27429dc373e82 /dev/include | |
| parent | d2d1fe30e3defa18dd966bf8160df81fc1e72e31 (diff) | |
[coq] Adapt to coq/coq#6831.
This removes uses of `Loc.t` in favor of `CAst.t`.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions