aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/trie.ml
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-11-27 09:28:09 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-11-28 19:21:24 +0100
commit34815f0c8fae4c87798b18f7343c1f1afc3056eb (patch)
treedaaa3b44d5ae0016a6cbfb78f9582b170c080568 /lib/trie.ml
parent5d3f5c210aad8d73b007936e65694c401e66c7d0 (diff)
Tactic primitives: missing [advance] lead to spurious dangling goals.
Closes #3801.
Diffstat (limited to 'lib/trie.ml')
0 files changed, 0 insertions, 0 deletions