aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-08-26 13:23:37 +0200
committerMatej Kosik2016-08-26 13:23:37 +0200
commitab9d2406975aba499d52f559e3303b82ce72d8ca (patch)
treeb1bfd60f6a8c897f96bacda48eb43a782a369c76 /engine/termops.ml
parent69388fcd52b4a2aeefe843099c608d96defd1ce6 (diff)
CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which can be useful in general, and then simplifying "Printer.pr_named_decl" function
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions