-
Notifications
You must be signed in to change notification settings - Fork 12
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.
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
Add some snippets #47
Conversation
Which kind of Coq answer did cause problems ? Answers to simple requests as Print, About, etc. Or goal displaying ?
Envoyé de mon iPad
… Le 20 juil. 2021 à 12:31, Théo Zimmermann ***@***.***> a écrit :
I did some experiments locally. However, for some reason, I couldn't yet produce a PDF with the Coq answers, so I will use this PR to check if that's produced correctly.
You can view, comment on, or merge this pull request online at:
#47
Commit Summary
Expand .gitignore after #44.
Insert some new snippets extracted from the code.
File Changes
M .gitignore (3)
M doc/chapter-primrec.tex (28)
M doc/movies/Makefile (1)
M theories/ordinals/Ackermann/extEqualNat.v (4)
M theories/ordinals/MoreAck/PrimRecExamples.v (19)
Patch Links:
https://github.com/coq-community/hydra-battles/pull/47.patch
https://github.com/coq-community/hydra-battles/pull/47.diff
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.
|
Everything, but that's because my coq-serapi is not correctly installed. The problem doesn't show up in the version built by the CI. |
Ok, so it's safe to merge this PR to master now ? |
The |
OK, it worked! So this is ready to merge. |
How about adding in the pdf doc and README.md a paragraph like: |
Good idea |
I did some experiments locally. However, for some reason, I couldn't yet produce a PDF with the Coq answers, so I will use this PR to check if that's produced correctly.