aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\
* \ Merge PR #6568: Cleanup scriptsGravatar Maxime Dénès2018-01-23
|\ \
| | * Archive COMPATIBILITY.Gravatar Théo Zimmermann2018-01-22
| | |
* | | Merge PR #6550: Remove outdated note about rlwrap in setup.txtGravatar Maxime Dénès2018-01-22
|\ \ \ | |_|/ |/| |
* | | Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\ \ \
| | | * merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
| | | |
| | | * Source basic overlay before user overlays.Gravatar Gaëtan Gilbert2018-01-16
| | | |
| | | * Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
| | | |
| | | * Simplify logic and streamline lint-repository.shGravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* | | | Fix the wrapper around ocamldebug.Gravatar Pierre-Marie Pédrot2018-01-15
| | | | | | | | | | | | | | | | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug
* | | | Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \
| * | | | Adding a custom Travis overlay for HoTT.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | |
* | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelGravatar Maxime Dénès2018-01-10
|\ \ \ \ \ \ | |_|/ / / / |/| | | | |
| | | | | * Cleanup conditional in lint-repository.shGravatar Gaëtan Gilbert2018-01-08
| | | | | |
| | | | * | Stop talking about debian in "A note about rlwrap"Gravatar Gaëtan Gilbert2018-01-08
| | | | |/ | | | | | | | | | | | | | | | Debian stable version is 0.42-3 right now.
* | | | | Merge PR #6549: Normalize package namesGravatar Maxime Dénès2018-01-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6527: Update backport script for more control.Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \
| | | * | | | github-check-prs.py: print PR URLs when needed.Gravatar Gaëtan Gilbert2018-01-08
| | | | | | |
| | | * | | | github-check-prs.py: Strip spaces from token from command lineGravatar Gaëtan Gilbert2018-01-08
| | | | | | |
| | | * | | | github-check-prs.py: command line option to get token from a fileGravatar Gaëtan Gilbert2018-01-08
| | | | | | |
* | | | | | | Merge PR #6501: Document use of ocamldebug from the command line in ↵Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | | | | | | | | | Cygwin/Windows
| | | | | * | First stab at documenting the test suite.Gravatar Jasper Hugunin2018-01-06
| |_|_|_|/ / |/| | | | |
| | | * | | Normalize MacOS installer name.Gravatar Théo Zimmermann2018-01-04
| | | | | |
| | | * | | Normalize Windows installer names.Gravatar Théo Zimmermann2018-01-04
| |_|/ / / |/| | | |
| | | * | Expound on dependencies for github-check-prs.pyGravatar Gaëtan Gilbert2017-12-30
| | | | |
| | | * | Python script checking missing/unnecessary [needs: rebase] labelGravatar Gaëtan Gilbert2017-12-30
| | | | |
| * | | | Add instructions for debugging from the command line (and in Windows)Gravatar Jim Fehrle2017-12-29
| | | | | | | | | | | | | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
* | | | | Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6405: Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-29
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| | * | | | overlay for #6493Gravatar Enrico Tassi2017-12-27
| | | | | |
| | * | | | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| |/ / / / |/| | | | | | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* | | | | Merge PR #6102: Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
|\ \ \ \ \
| | * | | | Add equations overlay.Gravatar Maxime Dénès2017-12-27
| |/ / / / |/| | | |
| * | | | Fix #5998: AppVeyor package building is currently failingGravatar Maxime Dénès2017-12-27
| | | | |
* | | | | Merge PR #6507: [ide] [doc] Document tweak to Query call.Gravatar Maxime Dénès2017-12-27
|\ \ \ \ \
| * | | | | [ide] [doc] Document tweak to Query call.Gravatar Emilio Jesus Gallego Arias2017-12-26
| | |/ / / | |/| | |
* | | | | Fix overlay selection for Circle CI.Gravatar Gaëtan Gilbert2017-12-26
| | | | |
* | | | | Delete old overlays (leaving example)Gravatar Gaëtan Gilbert2017-12-26
|/ / / /
| | * / Update backport script for more control.Gravatar Théo Zimmermann2017-12-24
| |/ / |/| |
| | * Add printers to dev/dbGravatar Gaëtan Gilbert2017-12-22
| | |
| | * Reorder dev/dbGravatar Gaëtan Gilbert2017-12-22
| | |
| | * Cleanup top_printers.mliGravatar Gaëtan Gilbert2017-12-22
| | |
| | * Cleanup debug printers a bit, add generated mli.Gravatar Gaëtan Gilbert2017-12-22
| | |
* | | Merge PR #6318: Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-22
|\ \ \
* | | | Fix CI with parallel make (messed up dependencies)Gravatar Gaëtan Gilbert2017-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
| * | | Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* | | Merge PR #6400: Circle CIGravatar Maxime Dénès2017-12-19
|\ \ \
* \ \ \ Merge PR #6305: Build with windows line endingsGravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6217: Do dependencies in 1 command per file class.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \