aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-16Merge PR #7079: Remove naked pointers from the VMMaxime Dénès
2018-05-16Merge PR #7391: Add a small documentation writer's guideMaxime Dénès
2018-05-16Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ...Gaëtan Gilbert
2018-05-16Merge PR #7484: Fix non-portable shebang in test-suite.Enrico Tassi
2018-05-16Merge PR #7227: [ssr] import ssreflect test suite from math-compMaxime Dénès
2018-05-16Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.Emilio Jesus Gallego Arias
2018-05-16[travis] Remove some more jobs from PR testing now that they are on Gitlab.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7507: gitlab CI: fix [warnings] templateEmilio Jesus Gallego Arias
2018-05-16Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.Emilio Jesus Gallego Arias
2018-05-15Merge PR #7519: git / gpg integration linkThéo Zimmermann
2018-05-15Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation fu...Pierre-Marie Pédrot
2018-05-15[doc] More feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Search for 'coqtop' in $PATH if COQBIN is unsetClément Pit-Claudel
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
2018-05-15[doc] Clarify a comment in the READMEClément Pit-Claudel
2018-05-15[doc] Add an ELisp snippet to insert Sphinx roles and quotesClément Pit-Claudel
2018-05-15[doc] Add a README to doc/sphinx/Clément Pit-Claudel
2018-05-15[doc] Document all directives and roles of our Sphinx domainClément Pit-Claudel
2018-05-15[doc] Small fixesClément Pit-Claudel
2018-05-15[doc] Compute the path to coqdoc at run time, not at load timeClément Pit-Claudel
2018-05-15Update MERGING.mdMatthieu Sozeau
2018-05-15Update MERGING.mdMatthieu Sozeau
2018-05-15git / gpg integration linkMatthieu Sozeau
2018-05-15Merge PR #7213: Do not compute constr matching context if not used.Matthieu Sozeau
2018-05-15Merge PR #7487: Remove duplicate entries for Proof, Qed, Defined, Admitted.Maxime Dénès
2018-05-15Merge PR #7503: [ci] [circleci] Remove jobs done in Gitlab efficiently.Gaëtan Gilbert
2018-05-15[ssr] import ssreflect test suite from math-compEnrico Tassi
2018-05-15Merge PR #7224: Attempt to fix the doubly encapsulated Ltac errors in coqideEnrico Tassi
2018-05-14Merge PR #7190: Option for quick compilation of the reference manual, bypassi...Maxime Dénès
2018-05-14Merge PR #7506: Add GitLab CI badge in first position.Maxime Dénès
2018-05-14Merge PR #7504: Define code owners for more CI files.Maxime Dénès
2018-05-14Merge PR #7170: Script to identify the code owner for given filesMaxime Dénès
2018-05-14Update CI README with info about gitlab windows and docker jobs.Gaëtan Gilbert
2018-05-14Gitlab: skip docker job when $SKIP_DOCKER == "true".Gaëtan Gilbert
2018-05-14Gitlab: build docker image in pipeline and use through registry.Gaëtan Gilbert
2018-05-14Merge PR #7337: dir-locals: add bug-reference-mode variablesEmilio Jesus Gallego Arias
2018-05-14Merge PR #7482: Update CI documentation following recent evolutions.Emilio Jesus Gallego Arias
2018-05-14Merge PR #7502: Fixing little printing bug with "Locate" on recursive notationsEmilio Jesus Gallego Arias
2018-05-14Merge PR #7344: Windows packaging build with Gitlab CIGaëtan Gilbert
2018-05-14Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...Gaëtan Gilbert
2018-05-14Remove duplicate entries for Proof, Qed, Defined, Admitted.Théo Zimmermann
2018-05-14gitlab CI: fix [warnings] templateGaëtan Gilbert
2018-05-14Merge PR #7374: [sphinx] More fatal warnings.Maxime Dénès
2018-05-14Add GitLab CI badge in first position.Théo Zimmermann
2018-05-14Pick up user overlays when running GitLab CI on PRs.Théo Zimmermann
2018-05-14Define code owners for more CI files.Théo Zimmermann
2018-05-14Update CI documentation following recent evolutions.Théo Zimmermann
2018-05-14Merge PR #7365: Mini fixes in the tactics chapterMaxime Dénès
2018-05-14[ci] [circleci] Remove jobs done in Gitlab efficiently.Emilio Jesus Gallego Arias