diff options
author | 2016-08-26 13:11:51 +0200 | |
---|---|---|
committer | 2016-08-26 13:11:51 +0200 | |
commit | 6cdcd498c4b425cad077f5bfaa453dc605b325a2 (patch) | |
tree | d4948aa9bf43929226e384e7fccb8ef37cba1e86 /kernel/nativelib.ml | |
parent | f45bbcf79018da0f52098ae284af73a5d38249c3 (diff) |
CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions