aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/debugging.md
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-04-03 15:39:11 +0200
committerErik Martin-Dorel2019-04-23 20:22:40 +0200
commit36488400952da5e12c8af451b1a936a34b26039d (patch)
treedeaaf8bc97829427bf444c37ba08496874b7c356 /dev/doc/debugging.md
parent4bc91ba5654574d156ebf2934a6fb36d31b40ff9 (diff)
[ssr] under: optimization of the tactic for (under eq_bigl => *)
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over."
Diffstat (limited to 'dev/doc/debugging.md')
0 files changed, 0 insertions, 0 deletions