aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-03-05 22:10:45 +0100
committerEmilio Jesus Gallego Arias2018-03-10 00:32:50 +0100
commit123de18a0886233b047ef2bad4bd7b3694f2abcc (patch)
tree372ec9a7e74c3b1ea1a2cd834cc27429dc373e82 /kernel/nativecode.ml
parentd2d1fe30e3defa18dd966bf8160df81fc1e72e31 (diff)
[coq] Adapt to coq/coq#6831.
This removes uses of `Loc.t` in favor of `CAst.t`.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions