aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-02Fixing #8106 (anomaly if declaring levels for only printing then only parsing).Hugo Herbelin
Notations were not initially designed to support independent parsing and printing rules. Some redesign of this part of the code shall be necessary at some time.
2018-09-01Merge PR #8348: Download tarball instead of cloning external projects.Emilio Jesus Gallego Arias
2018-08-31Merge PR #8346: Clean-up Travis folds.Gaëtan Gilbert
2018-08-31Merge PR #8351: [ci] [docker] Update base Dune version.Gaëtan Gilbert
2018-08-31Merge PR #8170: Don't index names starting with `_` in docsThéo Zimmermann
2018-08-31Merge PR #8219: Refman consistency checkThéo Zimmermann
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
This allows to use fixed commits and not just branches or tags. We keep using git clone when $FORCE_GIT is set (for projects on gforge.inria.fr and projects pulling dependencies through git submodules). fiat-parsers also calls git submodule, but inside its own Makefile.
2018-08-31Merge PR #8368: [ci] Fix QuickChick by adding new simple-io dependency.Gaëtan Gilbert
2018-08-31[ci] Fix QuickChick by adding new simple-io dependency.Théo Zimmermann
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-30[ci] [docker] Update Dune and Elpi versions.Emilio Jesus Gallego Arias
We'd like to use `(lang 1.1)` features. Elpi needs update as recent `ppx_tools_versioned` changes broke it.
2018-08-30Merge PR #8354: Move CHANGES entry for #8167 to 8.8.2 sectionThéo Zimmermann
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 CHANGES entry for #8167 to 8.8.2 sectionJason Gross
As per https://github.com/coq/coq/pull/8167#issuecomment-416929865
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-28Clean-up Travis folds.Théo Zimmermann
This has become mostly garbage since GitLab CI became our main CI platform.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 23:40:06 +0000