aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorKenji Maillard2020-05-11 23:10:03 +0200
committerKenji Maillard2020-05-11 23:10:03 +0200
commitceb1f5676fa3fd5c1a0b06d45ec62626175d78aa (patch)
tree7c6afb41571711624db7927fcc2b35a29545e676 /kernel/nativecode.mli
parent6cb24494fe8b6e945c6b6696134a6a42ecdab6ec (diff)
More tests of rebinding Ltac2 definitions
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions