aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-17[STM] Nested Proofs Allowed has to be executed immediatelyEnrico Tassi
2018-05-17Remove deprecation warning for nested proofs.Théo Zimmermann
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-16Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.Maxime Dénès
2018-05-16Modify make system to include Makefile.common in the test suiteGaëtan Gilbert
2018-05-16[ci] Try to build more of fiat-crypto.Emilio Jesus Gallego Arias
2018-05-16Merge PR #7514: [ci] Don't build lite versions of CI developments.Gaëtan Gilbert
2018-05-16Merge PR #7535: Typo in documentation of DeriveThéo Zimmermann
2018-05-16Merge PR #7493: Minor update of the documentation about the rcfileEmilio Jesus Gallego Arias
2018-05-16Typo in documentation of DeriveJoachim Breitner
2018-05-16[sphinx] Bump timeout. Closes #7532.Clément Pit-Claudel
2018-05-16[sphinx] Fix mistake in index.Théo Zimmermann
2018-05-16[sphinx] Improve rewrite section in tactic chapter.Théo Zimmermann
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-16[windows] Don't make menhir and int anymore.Emilio Jesus Gallego Arias
2018-05-16unit tests: add .merlinGaëtan Gilbert
2018-05-16add unit tests to test suitePaul Steckler
2018-05-16Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ...Gaëtan Gilbert
2018-05-16Minor update of the documentation/man about the resource file.Hugo Herbelin
2018-05-16document 7025Enrico Tassi
2018-05-16[ssr] fix after to_constr ~abort_on_undefined_evars was addedEnrico Tassi
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[ci] Don't build lite versions of CI developments.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-16[ide] Don't set `quiet` on start.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-15Merge branch 'fast-constr-match-no-context'Pierre-Marie Pédrot
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-15[sphinx] Fix indentation at the end of proof handling chapter.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 05:34:20 +0000