aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-10-09 21:56:24 +0200
committerGaëtan Gilbert2020-10-26 14:42:15 +0100
commit30f97beb1bfc149d9608cb74f24f69f268671e04 (patch)
tree7423e52ead0509a4496fc40741664867d26db2ed /kernel/nativecode.ml
parent5146b2f01b3b901ac99823d3a448c77560f248db (diff)
Ltac2: use ComTactic infrastructure
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions