aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorHugo Herbelin2017-12-06 08:58:50 +0100
committerMaxime Dénès2018-03-08 21:58:26 +0100
commitd2c50bb29df8f0b23f7ee498abeda43a672fc688 (patch)
tree127379b1d724f5b7b76f2b0a48a942cc7552f35e /dev/base_include
parent866bad4e9cdaa6ff4419840f8c9980f770873176 (diff)
Proof engine: consider the pair principal and future goals as an entity.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions