aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-04-13 16:44:22 +0200
committerMatthieu Sozeau2015-04-13 16:48:07 +0200
commita3d686a3bd1ac4256279a77c291949a3b15abc18 (patch)
tree8b856f81fbf3edd04c21595e5ec970d07b2ce55a /dev/base_include
parent546e2454f244340694f8fca460598499359afe28 (diff)
Program: Do not reduce obligation types preemptively, only at
definition time. The obligation tactic or user can still choose to do so.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions