aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-15 10:51:08 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-15 14:42:29 +0100
commitcedcfc9bc386456f3fdd225f739706e4f7a2902c (patch)
treec8161338a95bebdab6501606edda5a0a939da4a0 /plugins
parent8b15e47a6b3ccae696da8e12dbad81ae0a740782 (diff)
Refine tactic now shelves unifiable holes.
The unshelve tactical can be used to get the shelved holes. This changes the proper ordering of holes though, so expect some broken scripts. Also, the test-suite is not fixed yet.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions