aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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
|\ \ \ | |_|/ |/| |
* | | 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
| |/ |/|
* | 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
|\ \ \ \
* \ \ \ \ Merge PR #6419: [vernac] Split `command.ml` into separate files.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ \
| | * | | | | [vernac] Split `command.ml` into separate files.Gravatar Emilio Jesus Gallego Arias2017-12-17
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.
| | | * | | Fix build fileGravatar Jim2017-12-16
| | | | | |
| | * | | | Overlay for unimath.Gravatar Gaëtan Gilbert2017-12-15
| | | | | |
* | | | | | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| | * | | | [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| |/ / / / | | | | | | | | | | | | | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
* | | | | Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | | | | * Put bignums, math-classes and corn dependencies in MakefileGravatar Gaëtan Gilbert2017-12-13
| | | | | | |
| | | * | | | [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding.
* | | / | | Revert "[ci] Temporal workaround for checker non-backwards compatible change."Gravatar Théo Zimmermann2017-12-12
| |_|/ / / |/| | | | | | | | | | | | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
* | | | | Merge PR #6331: Linter: skip PRs older than the linter.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | Add overlay.Gravatar Théo Zimmermann2017-12-11
| |_|/ / |/| | |
* | | | Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\ \ \ \
* \ \ \ \ Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.Gravatar Maxime Dénès2017-12-11
|\ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 12:38:56 +0000