aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-08-30Merge PR #8349: Mention dev/doc/critical-bugs in CONTRIBUTINGThéo Zimmermann
2018-08-30Merge PR #8292: Create SPHINXWARNERROR variable to control Sphinx "warn as ↵Théo Zimmermann
error" argument in make
2018-08-29Merge PR #8353: [sphinx] Fix timeout issue by splitting imports.Clément Pit-Claudel
2018-08-29Merge PR #8345: Add index for focusing braces.Clément Pit-Claudel
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
"treat errors as warnings" flag (-W) is applied. "1" or undefined includes the flag, other values or undefined omit it. Removed the "-warn-error" parameter to configure. "-profile XXX" will no longer cause these flags to be used.
2018-08-29Move mention of dev/doc/critical-bugs to CONTRIBUTINGJason Gross
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
2018-08-29Mention dev/doc/critical-bugs in the PR templateJason Gross
2018-08-29[sphinx] Fix timeout issue by splitting imports.Théo Zimmermann
2018-08-29Merge PR #8274: Restore previous printing filtering; always reprint the ↵Emilio Jesus Gallego Arias
context after "Set Diffs"
2018-08-29Merge PR #8313: [ci-fiat-crypto] Test extractionEmilio Jesus Gallego Arias
2018-08-29Merge PR #8350: Fix typo in comment, sollicited --> solicited.Emilio Jesus Gallego Arias
2018-08-29Merge PR #8282: [coq_makefile] print all options (Fix #7529)Théo Zimmermann
2018-08-29Merge PR #8167: Fix ordering of before/after in print-pretty-timed-*Enrico Tassi
2018-08-29Merge PR #8340: Put camldevfiles targets in MakefileEnrico Tassi
2018-08-28Merge PR #8334: Fix a casing problem noticed by Lars Dölle on Coq-Club.Clément Pit-Claudel
2018-08-28Fix typo in comment, sollicited --> solicited.Nick Lewycky
2018-08-28[ci-fiat-crypto] Build c-filesJason Gross
This tests the outputs of extraction, to some extent.
2018-08-28Merge PR #8135: Sphinx fixing of the beginning of the Tactics chapter.Clément Pit-Claudel
2018-08-28Merge PR #8281: Trivial Sphinx fix in doc.Clément Pit-Claudel
2018-08-28Add index for focusing braces.Théo Zimmermann
And fix wrong indentation.
2018-08-28Merge PR #8333: Fix URIs in the configuration scriptEmilio Jesus Gallego Arias
2018-08-28Put camldevfiles targets in MakefileGaëtan Gilbert
There's no need to build dependencies for it.
2018-08-28Merge PR #8112: Add support for focusing on named goals using brackets.Pierre-Marie Pédrot
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-27Merge PR #8312: Split up fiat-crypto CI into two targetsGaëtan Gilbert
2018-08-27Merge PR #8260: Tweak diff options in CoqIDEPierre-Marie Pédrot
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
2018-08-27Merge PR #8293: Fix typo of caracterisation -> c*h*aracterisationHugo Herbelin
2018-08-27Fix wwwrefman and wwwstdlibKazuhiko Sakaguchi
2018-08-24Bug fix: restore previous printing behavior that was unintentionally changed ↵Jim Fehrle
in 7d2a9df (current code always prints context, should print only if the proof has changed). Bug fix: Fix message that came out as "Error: Error: -diffs requires ..." Enhancement: always print the context after the "Set Diffs" command.
2018-08-24Merge PR #8266: Minor Sphinx improvements in the bullet documentation.Clément Pit-Claudel
2018-08-24Fix ordering of before/after in print-pretty-timed-*Jason Gross
Fixes #8158
2018-08-24Split up fiat-crypto CI into two targetsJason Gross
There is the new pipeline, and the old pipeline. Most of what they share in common is the (very large) library of lemmas about `Z`. As per the discussion in https://github.com/coq/coq/pull/8064#issuecomment-413474176 through https://github.com/coq/coq/pull/8064#issuecomment-413793143
2018-08-23Merge PR #8296: Fix #8251: remove "the the" occurrencesThéo Zimmermann
2018-08-23Merge PR #8300: Fix issue #8298 OCaml 4.07 download path is incorrectThéo Zimmermann
2018-08-22Fix issue #8298 OCaml 4.07 download path is incorrectMichael Soegtrop
2018-08-22Fix #8251: remove "the the" occurrencesGaëtan Gilbert
2018-08-22Fix typo of caracterisation -> c*h*aracterisationSiddharth Bhat
2018-08-22Add missing spaces.Théo Zimmermann
2018-08-22[sphinx] Improve Case analysis and induction section.Théo Zimmermann
2018-08-22[refman] Fixing two nested lemma errors.Théo Zimmermann
2018-08-22[sphinx] Fixing of the beginning of the Tactics chapter.Théo Zimmermann
2018-08-21Merge PR #8249: Remove unneeded file stm/workerLoop.mliEnrico Tassi
2018-08-21[coq_makefile] print all options (Fix #7529)Enrico Tassi
2018-08-21Trivial Sphinx fix in doc.Théo Zimmermann
2018-08-20Merge PR #8258: Update documentation on GitLab CI to reflect recent changes.Emilio Jesus Gallego Arias
2018-08-20Merge PR #8136: Do not run 32-bit Windows builds on pull requests.Emilio Jesus Gallego Arias
2018-08-20Merge PR #8262: Remove dead argument allow_old.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 12:58:14 +0000