aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #6808: Add unit tests to test-suiteGravatar Gaëtan Gilbert2018-05-17
|\
* \ Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Gravatar Maxime Dénès2018-05-16
|\ \
| | * Modify make system to include Makefile.common in the test suiteGravatar Gaëtan Gilbert2018-05-16
* | | Merge PR #7514: [ci] Don't build lite versions of CI developments.Gravatar Gaëtan Gilbert2018-05-16
|\ \ \
* \ \ \ Merge PR #7535: Typo in documentation of DeriveGravatar Théo Zimmermann2018-05-16
|\ \ \ \
* \ \ \ \ Merge PR #7493: Minor update of the documentation about the rcfileGravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \
| | * | | | Typo in documentation of DeriveGravatar Joachim Breitner2018-05-16
| |/ / / / |/| | | |
* | | | | Merge PR #7079: Remove naked pointers from the VMGravatar Maxime Dénès2018-05-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7391: Add a small documentation writer's guideGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \
| | | | | | * unit tests: add .merlinGravatar Gaëtan Gilbert2018-05-16
| | | | | | * add unit tests to test suiteGravatar Paul Steckler2018-05-16
| |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ...Gravatar Gaëtan Gilbert2018-05-16
|\ \ \ \ \ \
| | | | * | | Minor update of the documentation/man about the resource file.Gravatar Hugo Herbelin2018-05-16
* | | | | | | Merge PR #7484: Fix non-portable shebang in test-suite.Gravatar Enrico Tassi2018-05-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7227: [ssr] import ssreflect test suite from math-compGravatar Maxime Dénès2018-05-16
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \
| | | | | | | | * | [ci] Don't build lite versions of CI developments.Gravatar Emilio Jesus Gallego Arias2018-05-16
| | | | * | | | | | [travis] Remove some more jobs from PR testing now that they are on Gitlab.Gravatar Emilio Jesus Gallego Arias2018-05-16
| |_|_|/ / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7507: gitlab CI: fix [warnings] templateGravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Gravatar Emilio Jesus Gallego Arias2018-05-16
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7519: git / gpg integration linkGravatar Théo Zimmermann2018-05-15
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation fu...Gravatar Pierre-Marie Pédrot2018-05-15
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | [doc] More feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Search for 'coqtop' in $PATH if COQBIN is unsetGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Address feedback on doc writer guideGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Clarify a comment in the READMEGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Add an ELisp snippet to insert Sphinx roles and quotesGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Add a README to doc/sphinx/Gravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Document all directives and roles of our Sphinx domainGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Small fixesGravatar Clément Pit-Claudel2018-05-15
| | | | | | | | * | | | | [doc] Compute the path to coqdoc at run time, not at load timeGravatar Clément Pit-Claudel2018-05-15
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | |
| | * | | | | | | | | | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | * | | | | | | | | | Update MERGING.mdGravatar Matthieu Sozeau2018-05-15
| | * | | | | | | | | | git / gpg integration linkGravatar Matthieu Sozeau2018-05-15
| | | |_|_|_|_|_|_|/ / | | |/| | | | | | | |
* | | | | | | | | | | Merge PR #7213: Do not compute constr matching context if not used.Gravatar Matthieu Sozeau2018-05-15
|\ \ \ \ \ \ \ \ \ \ \ | |_|/ / / / / / / / / |/| | | | | | | | | |
| | | | | | | | | | * [sphinx] Fix indentation at the end of proof handling chapter.Gravatar Théo Zimmermann2018-05-15
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
* | | | | | | | | | Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.Gravatar Maxime Dénès2018-05-15
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7503: [ci] [circleci] Remove jobs done in Gitlab efficiently.Gravatar Gaëtan Gilbert2018-05-15
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | [ssr] import ssreflect test suite from math-compGravatar Enrico Tassi2018-05-15
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqideGravatar Enrico Tassi2018-05-15
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7190: Option for quick compilation of the reference manual, bypassi...Gravatar Maxime Dénès2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7506: Add GitLab CI badge in first position.Gravatar Maxime Dénès2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7504: Define code owners for more CI files.Gravatar Maxime Dénès2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7170: Script to identify the code owner for given filesGravatar Maxime Dénès2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | Update CI README with info about gitlab windows and docker jobs.Gravatar Gaëtan Gilbert2018-05-14
| | | | | | | | | | | | * | | | Gitlab: skip docker job when $SKIP_DOCKER == "true".Gravatar Gaëtan Gilbert2018-05-14
| | | | | | | | | | | | * | | | Gitlab: build docker image in pipeline and use through registry.Gravatar Gaëtan Gilbert2018-05-14
| |_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR #7337: dir-locals: add bug-reference-mode variablesGravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7482: Update CI documentation following recent evolutions.Gravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7502: Fixing little printing bug with "Locate" on recursive notationsGravatar Emilio Jesus Gallego Arias2018-05-14
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:39:11 +0000