aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-10-08 17:26:31 +0200
committerMatthieu Sozeau2014-10-10 20:40:04 +0200
commit32653d69478992d55dc45a5562aeb6b41ae67f21 (patch)
tree16e4c932b8a0a50bac85174dfc893a857a5f4f38 /dev
parent4dca32d9eabd2c5a1a239cfb8c3a33a0d962991c (diff)
Add a "Debug Tactic Unification" option and correct the first-order
application case to expand primitive projections at the head of both applications.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions