Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7898: Remove camlp4 remains | 2018-07-11 | |
|\ | |||
* | | Add new options --no-conflict and --no-signature-check to backport script. | 2018-07-10 | |
| | | |||
* | | Modify URLs in xml-protocol.md | 2018-07-08 | |
| | | |||
* | | Modify URLs in xml-protocol.md | 2018-07-08 | |
| | | |||
| * | Add an overlay. | 2018-07-07 | |
| | | |||
| * | Introduce a Pcoq.Entry module for functions that ought to be exported. | 2018-07-07 | |
|/ | | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins. | ||
* | Merge PR #7746: Many small cleanups removing unused arguments and functions | 2018-07-05 | |
|\ | |||
* \ | Merge PR #7979: TACTIC EXTEND in coqpp | 2018-07-05 | |
|\ \ | |||
* | | | [ci] Avoid annoying detached head warning. | 2018-07-04 | |
| | | | |||
* | | | Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵ | 2018-07-03 | |
|\ \ \ | | | | | | | | | | | | | with apt. | ||
| | | * | Add overlay for equations. | 2018-07-03 | |
| |_|/ |/| | | |||
* | | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | 2018-07-03 | |
|\ \ \ | |||
| | * | | [ci] [docker] Make sure we don't install optional packages with apt. | 2018-07-02 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them. | ||
| | | * | Documenting the syntax changes. | 2018-07-02 | |
| | |/ | |||
| * / | Add Equations overlay | 2018-07-02 | |
| |/ | |||
* / | Clean up documentation around beginner's guide. | 2018-07-02 | |
|/ | | | | | | | | | - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`. | ||
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | 2018-07-02 | |
|\ | | | | | | | points of Camlp5 | ||
* \ | Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵ | 2018-07-01 | |
|\ \ | | | | | | | | | | .git anymore. | ||
* \ \ | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵ | 2018-07-01 | |
|\ \ \ | | | | | | | | | | | | | Z into three files | ||
| | | * | Adding an overlay for the PR. | 2018-06-29 | |
| | | | | |||
| | | * | Documenting the transition strategy of GEXTEND. | 2018-06-29 | |
| |_|/ |/| | | |||
| | * | Document that GITURL variables shouldn't have a trailing .git anymore. | 2018-06-29 | |
| |/ |/| | | | | | This allows to append /archive at the end. | ||
* | | Merge PR #7918: Mini-update of version history with recent changes. | 2018-06-29 | |
|\ \ | |||
| | * | Splitting primitive numeral parser/printer for positive, N, Z into three files. | 2018-06-29 | |
| | | | |||
* | | | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵ | 2018-06-29 | |
|\ \ \ | | | | | | | | | | | | | constr in Constr | ||
* \ \ \ | Merge PR #7745: Make type Environ.globals abstract + simplify ↵ | 2018-06-29 | |
|\ \ \ \ | |_|_|/ |/| | | | | | | | Environ.retroknowledge | ||
* | | | | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs. | 2018-06-28 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine. | 2018-06-28 | |
|\ \ \ \ \ | |||
| | | * | | | Make Environ.globals abstract. | 2018-06-28 | |
| |_|/ / / |/| | | | | |||
* | | | | | Add mit-plv/bedrock2-ci to CI | 2018-06-27 | |
| | | | | | |||
| | | * | | Adding overlay. | 2018-06-27 | |
| | | | | | |||
| | | * | | Swapping Context and Constr: defining declarations on constr in Constr. | 2018-06-27 | |
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate). | ||
| | * | | Fix 'unbound variable' issue on Windows packaging jobs. | 2018-06-27 | |
| | | | | |||
* | | | | Merge PR #7863: Remove Sorts.contents | 2018-06-27 | |
|\ \ \ \ | |_|/ / |/| | | | |||
* | | | | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | 2018-06-26 | |
|\ \ \ \ | | | | | | | | | | | | | | | | constants | ||
* \ \ \ \ | Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵ | 2018-06-26 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | build | ||
* \ \ \ \ \ | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | 2018-06-26 | |
|\ \ \ \ \ \ | |||
| | | | * | | | Add overlay for elpi | 2018-06-26 | |
| | | | | | | | |||
| | | | * | | | Remove Sorts.contents | 2018-06-26 | |
| |_|_|/ / / |/| | | | | | |||
| | | * | | | Add overlay for Equations, Elpi | 2018-06-26 | |
| | | | | | | |||
| | * | | | | Activate the build of Ltac2 and Equations in the Windows installer. | 2018-06-25 | |
| | | | | | | |||
| | * | | | | Reuse CI info to know which version of plugins to build on Windows. | 2018-06-25 | |
| | | | | | | |||
| | * | | | | Fix for issue 7707: include Ltac2 and Equations in Windows build | 2018-06-25 | |
| |/ / / / |/| | | | | | | | | | | | | | | On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin. | ||
| | | | * | Mini-update of version history with recent changes. | 2018-06-25 | |
| |_|_|/ |/| | | | |||
| | | * | Critical bugs: added #3243 and Gonthier's bug in lazy machine. | 2018-06-25 | |
| |_|/ |/| | | | | | | | | Both reminded by Enrico. | ||
* | | | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." | 2018-06-24 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. | 2018-06-24 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7893: Update dpdgraph branch name | 2018-06-22 | |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| | | * | | Revert "Add a note about [ci skip] in CI README." | 2018-06-22 | |
| |_|/ / |/| | | | | | | | | | | | This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d. | ||
| | | * | Fix Windows install script following removal of INSTALL.ide and move of ↵ | 2018-06-22 | |
| |_|/ |/| | | | | | | | | INSTALL.doc. |