aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix an anomaly when calling Obligation 0 or Obligation -1.Gravatar Théo Zimmermann2018-05-21
* Merge PR #7557: Add test cases from #7554Gravatar Théo Zimmermann2018-05-20
|\
| * Add test cases from #7554Gravatar Tej Chajed2018-05-20
* | Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging...Gravatar Michael Soegtrop2018-05-19
|\ \
* \ \ Merge PR #7550: [CI] Fix the script used by math-classes.Gravatar Emilio Jesus Gallego Arias2018-05-18
|\ \ \ | |_|/ |/| |
* | | Merge PR #6965: [api] Move universe syntax to `Glob_term`Gravatar Pierre-Marie Pédrot2018-05-18
|\ \ \
| | * | [CI] Fix the script used by math-classes.Gravatar Pierre-Marie Pédrot2018-05-18
| |/ / |/| |
* | | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...Gravatar Emilio Jesus Gallego Arias2018-05-17
|\ \ \
* \ \ \ Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\ \ \ \
* \ \ \ \ Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...Gravatar Pierre-Marie Pédrot2018-05-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6870: [ide] Don't set `quiet` on start.Gravatar Enrico Tassi2018-05-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7525: [ci] Try to build more of fiat-crypto.Gravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6808: Add unit tests to test-suiteGravatar Gaëtan Gilbert2018-05-17
|\ \ \ \ \ \ \ \
| | | | | | * | | Document nested proofs and associated option.Gravatar Théo Zimmermann2018-05-17
| | | | | | * | | [STM] Nested Proofs Allowed has to be executed immediatelyGravatar Enrico Tassi2018-05-17
| | | | | | * | | Remove deprecation warning for nested proofs.Gravatar Théo Zimmermann2018-05-17
| | | | | | * | | Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-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
| | | * | | | | | [ci] Try to build more of fiat-crypto.Gravatar Emilio Jesus Gallego Arias2018-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
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * [windows] Don't make menhir and int anymore.Gravatar Emilio Jesus Gallego Arias2018-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
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | [ide] Don't set `quiet` on start.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
| |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 05:23:09 +0000