aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-03 15:50:43 +0200
committerThéo Zimmermann2020-04-03 15:50:43 +0200
commit716262faefe4ea0975eea6e125bad2dfdaaf22ba (patch)
tree16c1ba223046a0854b7a7ffd43bc9041071208d1 /kernel/nativevalues.ml
parentacefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff)
Extract section on implicit arguments from Gallina extensions.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions