aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #7324: Infrastructure for ocamldebug on the checkerGravatar Hugo Herbelin2018-05-22
|\
* \ Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gravatar Gaëtan Gilbert2018-05-22
|\ \
* \ \ Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span mu...Gravatar Gaëtan Gilbert2018-05-22
|\ \ \
* \ \ \ Merge PR #6859: [stm] Make toplevels standalone executables.Gravatar Théo Zimmermann2018-05-22
|\ \ \ \
| | * | | [ci] [gitlab] Fix printenv sorting for variables that span multiple lines.Gravatar Emilio Jesus Gallego Arias2018-05-21
| |/ / / |/| | |
| * | | [ide] Remove special option `-ideslave`Gravatar Emilio Jesus Gallego Arias2018-05-21
| * | | [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| * | | [ci] Add Dune to the base system.Gravatar Emilio Jesus Gallego Arias2018-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
| |/ / / / |/| | | |
| | | * | [circle] Use Docker image from Gitlab registry.Gravatar Emilio Jesus Gallego Arias2018-05-17
| |_|/ / |/| | |
* | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 11:34:19 +0000