Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Improve PG support of Show Proof Diffs #490

Merged
merged 13 commits into from
May 29, 2020
Merged

Improve PG support of Show Proof Diffs #490

Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8e12eee
First try for feature #487
CyrilAnac May 11, 2020
ecb4747
All case for Show and regex variable
CyrilAnac May 14, 2020
aba3f2b
Fix name clash & rephrase some strings
erikmd May 15, 2020
04aff70
WIP for #487
CyrilAnac May 18, 2020
22681a3
Apply reviews of @erikmd
CyrilAnac May 20, 2020
ff9b5b1
test: Add regression test (currently failing)
erikmd May 20, 2020
411ebb2
fix: Do "Show Proof…" (with "?Goal") as soon as the proof is started
erikmd May 20, 2020
3ab3f5e
fix: backtrack wrong type argument
CyrilAnac May 25, 2020
8627fba
fix: backtrack for "Show Proof" disabled
CyrilAnac May 28, 2020
5b1b8ac
Add tests and flags system
CyrilAnac May 28, 2020
cc4b4f6
Fix the test 081
CyrilAnac May 28, 2020
77fd293
Minor changes
CyrilAnac May 29, 2020
9c82b71
refactor: Remove unneeded coq-should-response
erikmd May 29, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix the test 081
  • Loading branch information
@CyrilAnac
CyrilAnac committed May 29, 2020
commit cc4b4f6cd626cc6a2f02d3e4efe95dc84d577e3b
5 changes: 4 additions & 1 deletion ci/coq-tests.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,10 @@ For example, COMMENT could be (*test-definition*)"
(coq-test-goto-before " (*test-insert*)")
(proof-goto-point)
(proof-shell-wait)
(coq-should-buffer "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>"))
;; If coq--post-v811, it should be "Show Proof Diffs." otherwise "Show Proof."
(if (coq--post-v811)
(coq-should-buffer "<diff\\.added\\.bg>(fun <diff\\.added>(</diff\\.added>A : Prop<diff\\.added>) (proof_of_A : A)</diff\\.added> => \\?Goal)</diff\\.added\\.bg>")
CyrilAnac marked this conversation as resolved.
Show resolved Hide resolved
(coq-should-buffer "(fun (A : Prop) (proof_of_A : A) => \\?Goal)")))
'show-proof-stepwise 'diffs-on))


Expand Down