diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-25 19:50:33 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 19:50:33 -0400 |
| commit | 4a7d857dfb7733c103d944dfad82bd688037f721 (patch) | |
| tree | 4906771e1164e5154aa14df4da0b8f209befafd5 /folkwisdom.md | |
| parent | a31c716507d5373251dbd1ddfaf6f8e4f83d3a0a (diff) | |
actually fix pose proof
Diffstat (limited to 'folkwisdom.md')
| -rw-r--r-- | folkwisdom.md | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index 3530a517a..2234af646 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -208,11 +208,11 @@ sometimes even gives sensible error messages in Coq 8.5) but revert to `rewrite` once the issue has been found and fixed. If rewriting picks the wrong `Equivalence` or `Proper` instance for some type or function (or fails to find one altogether), troubleshoot that separately: check that `pose proof -(_:@Equivalence T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right -answer, and if not, `Set Typeclasses Debug` and read the log (which is in the -hidden `*coq*` buffer in Proof General). A useful heuristic for reading that log -is to look for the first place where the resolution backtracks and then read -backwards from there. +(_:@Equivalence T equiv)` or `pose proof (_:Proper (equiv1==>equiv2) f)` give +the right answer, and if not, `Set Typeclasses Debug` and read the log (which is +in the hidden `*coq*` buffer in Proof General). A useful heuristic for reading +that log is to look for the first place where the resolution backtracks and then +read backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call `(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold |