aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-27 18:29:39 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-27 18:29:39 +0200
commitc33988dafcad14f9f0c10a287d2cfb2790e253c4 (patch)
treeeba36b138067491f49fd12656df98d73ac8e7742 /kernel
parent04e0f9fde8789a28b66f24000ac8c831ff0815af (diff)
parent8d9b66bed22364f513771e9b1fa3df14a3dab866 (diff)
Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions