| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-06 | Merge PR #8073: Use GitHub as the location for OCaml sources. | Michael Soegtrop | |
| 2018-07-27 | [ci] Remove CircleCI setup. | Emilio Jesus Gallego Arias | |
| GitLab setup is quite stable these days thanks to the work of many people and `coqbot`. We decided to keep CircleCI support for a while as a safeguard in case something happened in the migration to GitLab, but these days we are just wasting resources to them and to us. As I'm afraid CircleCI won't scale for us, the time to remove it has arrived. Still, CircleCI had some awesome functionality that GitLab's CI doesn't offer yet, see the links at: https://github.com/coq/coq/issues/6919#issuecomment-395885573 - https://gitlab.com/gitlab-org/gitlab-ce/issues/29347 - https://gitlab.com/gitlab-org/gitlab-ce/issues/35222 - https://gitlab.com/gitlab-org/gitlab-ce/issues/41947 - https://gitlab.com/gitlab-org/gitlab-ce/issues/47063 | |||
| 2018-07-25 | Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in ↵ | Pierre-Marie Pédrot | |
| errors | |||
| 2018-07-25 | Merge PR #734: [travis] Also run coqchk on HoTT | Emilio Jesus Gallego Arias | |
| 2018-07-25 | Add overlay for Equations | Gaëtan Gilbert | |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin | |
| 2018-07-24 | [travis] Also run coqchk on HoTT | Jason Gross | |
| 2018-07-24 | Add overlay for Equations. | Gaëtan Gilbert | |
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-07-19 | Merge PR #7941: Extend QuestionMark to produce a better error message in ↵ | Pierre-Marie Pédrot | |
| case of missing record field | |||
| 2018-07-18 | Merge PR #8054: [dev] Autogenerate OCaml dev files. | Enrico Tassi | |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-17 | Add overlay for Coq-Equations for QuestionMark. | Siddharth Bhat | |
| The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this. | |||
| 2018-07-16 | Add overlay for QuickChick | Jason Gross | |
| 2018-07-16 | Only check overlay extensions on git-tracked files | Jason Gross | |
| This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git. | |||
| 2018-07-15 | Use GitHub as the location for OCaml sources. | Théo Zimmermann | |
| It will be more robust and more secure than downloading from the OCaml website. | |||
| 2018-07-12 | [dev] Autogenerate OCaml dev files. | Emilio Jesus Gallego Arias | |
| For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579 | |||
| 2018-07-12 | Merge PR #8051: Clean-up user-overlays folder. | Emilio Jesus Gallego Arias | |
| 2018-07-12 | Clean-up user-overlays folder. | Théo Zimmermann | |
| 2018-07-11 | [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0 | Emilio Jesus Gallego Arias | |
| - We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0. | |||
| 2018-07-11 | Merge PR #7898: Remove camlp4 remains | Emilio Jesus Gallego Arias | |
| 2018-07-10 | Add new options --no-conflict and --no-signature-check to backport script. | Théo Zimmermann | |
| 2018-07-08 | Modify URLs in xml-protocol.md | Rin Arakaki | |
| 2018-07-08 | Modify URLs in xml-protocol.md | Rin Arakaki | |
| 2018-07-07 | Add an overlay. | Pierre-Marie Pédrot | |
| 2018-07-07 | Introduce a Pcoq.Entry module for functions that ought to be exported. | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-07-05 | Merge PR #7746: Many small cleanups removing unused arguments and functions | Pierre-Marie Pédrot | |
| 2018-07-05 | Merge PR #7979: TACTIC EXTEND in coqpp | Emilio Jesus Gallego Arias | |
| 2018-07-04 | [ci] Avoid annoying detached head warning. | Emilio Jesus Gallego Arias | |
| 2018-07-03 | Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵ | Gaëtan Gilbert | |
| with apt. | |||
| 2018-07-03 | Add overlay for equations. | Gaëtan Gilbert | |
| 2018-07-03 | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | Pierre-Marie Pédrot | |
| 2018-07-02 | [ci] [docker] Make sure we don't install optional packages with apt. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2018-07-02 | Documenting the syntax changes. | Pierre-Marie Pédrot | |
| 2018-07-02 | Add Equations overlay | Matthieu Sozeau | |
| 2018-07-02 | Clean up documentation around beginner's guide. | Siddharth Bhat | |
| - 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`. | |||
| 2018-07-02 | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | Emilio Jesus Gallego Arias | |
| points of Camlp5 | |||
| 2018-07-01 | Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵ | Emilio Jesus Gallego Arias | |
| .git anymore. | |||
| 2018-07-01 | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵ | Emilio Jesus Gallego Arias | |
| Z into three files | |||
| 2018-06-29 | Adding an overlay for the PR. | Pierre-Marie Pédrot | |
| 2018-06-29 | Documenting the transition strategy of GEXTEND. | Pierre-Marie Pédrot | |
| 2018-06-29 | Document that GITURL variables shouldn't have a trailing .git anymore. | Théo Zimmermann | |
| This allows to append /archive at the end. | |||
| 2018-06-29 | Merge PR #7918: Mini-update of version history with recent changes. | Théo Zimmermann | |
| 2018-06-29 | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin | |
| 2018-06-29 | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵ | Maxime Dénès | |
| constr in Constr | |||
| 2018-06-29 | Merge PR #7745: Make type Environ.globals abstract + simplify ↵ | Maxime Dénès | |
| Environ.retroknowledge | |||
| 2018-06-28 | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs. | Michael Soegtrop | |
| 2018-06-28 | Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine. | Théo Zimmermann | |
| 2018-06-28 | Make Environ.globals abstract. | Gaëtan Gilbert | |
| 2018-06-27 | Add mit-plv/bedrock2-ci to CI | Andres Erbsen | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |