aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-04-22 17:26:03 +0200
committerGaëtan Gilbert2018-07-24 13:49:18 +0200
commita30be8ca7d6b7c6f17aa65de824e02194a7f3a9b (patch)
tree9b43febeca66aa4e8914ac90f9089f87f090da6c /kernel
parent0108db19c96e1b46346f032964f2cca3f8149cb3 (diff)
Fix #7329: coqchk Include with primitive projections
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions