diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:59:18 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:59:18 -0400 |
| commit | e61d477caa079526842d23a24aba4bdd9a2a8362 (patch) | |
| tree | 4a83696c16bee2b71657847bc16becc84387e49a /folkwisdom.md | |
| parent | 1554ea63676e285b8e8959bba6331a5ad11810d6 (diff) | |
s/`proofgeneral`/Proof General/
Diffstat (limited to 'folkwisdom.md')
| -rw-r--r-- | folkwisdom.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index 4f6d354eb..a41d1532f 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -210,8 +210,8 @@ once the issue has been found and fixed. If rewriting picks the wrong 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 `proofgeneral`). A useful heuristic for reading that -log is to look for the first place where the resolution backtracks and then read +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 |