aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-17 15:12:02 +0200
committerHugo Herbelin2014-10-17 15:12:05 +0200
commitbc8a5357889396f07d005a84bd3c50e9a25c1ddb (patch)
tree63bd14d10d345d9a1548626301632d8deb833835 /printing/printer.ml
parent239cf334fcc844f06a9e6ea2e6745d2fa8915325 (diff)
New experimental heuristic printing strategy for evar instances: We
don't print bindings of the form "x:=x" unless there is also a binding "x':=x". Otherwise said, if a variable occurs several time, the binding where it occurs under the form "x:=x" is printed anyway. This should help to understand where the instance is non trivial while still not obfuscating display in goals with very long list of uninteresting trivial instances.
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions