diff options
| author | Erik Martin-Dorel | 2020-05-29 19:56:44 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-29 19:56:44 +0200 |
| commit | 5ba7aee8a8996b8219a6e9dbde645e53684afbca (patch) | |
| tree | 297503b50c51cc04a60609e42e6140d4ed2177de /coq/coq-syntax.el | |
| parent | 0bfd208037646a1e1871dae9fc6fc6be0f7bd39c (diff) | |
| parent | 9c82b71d396b425337592f96f2e9b6a1d97be0c0 (diff) | |
Merge pull request #490 from ProofGeneral/feature/487
Improve PG support of Show Proof (Diffs):
Display the proof terms stepwise in the *response* buffer.
Close #487
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 470331a6..5b8d8c48 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,6 +1304,9 @@ It is used: "*Font-lock table for Coq terms.") +(defconst coq-show-proof-diffs-regexp + "\\`Show Proof\\(?: Diffs\\| Diffs removed\\)?\\.\\'") + (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. (concat "\\`\\(\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\_<" |