Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands | Pierre-Marie Pédrot | 2018-07-03 |
|\ | |||
| * | Add Equations overlay | Matthieu Sozeau | 2018-07-02 |
| | | |||
* | | Clean up documentation around beginner's guide. | Siddharth Bhat | 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 ↵ | Emilio Jesus Gallego Arias | 2018-07-02 |
|\ | | | | | | | points of Camlp5 | ||
* \ | Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵ | Emilio Jesus Gallego Arias | 2018-07-01 |
|\ \ | | | | | | | | | | .git anymore. | ||
* \ \ | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵ | Emilio Jesus Gallego Arias | 2018-07-01 |
|\ \ \ | | | | | | | | | | | | | Z into three files | ||
| | | * | 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 | 2018-06-29 |
| |/ |/| | | | | | This allows to append /archive at the end. | ||
* | | 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 | 2018-06-29 |
|\ \ \ | | | | | | | | | | | | | constr in Constr | ||
* \ \ \ | Merge PR #7745: Make type Environ.globals abstract + simplify ↵ | Maxime Dénès | 2018-06-29 |
|\ \ \ \ | |_|_|/ |/| | | | | | | | Environ.retroknowledge | ||
* | | | | 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-28 |
| |_|/ / / |/| | | | | |||
* | | | | | Add mit-plv/bedrock2-ci to CI | Andres Erbsen | 2018-06-27 |
| | | | | | |||
| | | * | | Adding overlay. | Hugo Herbelin | 2018-06-27 |
| | | | | | |||
| | | * | | Swapping Context and Constr: defining declarations on constr in Constr. | Hugo Herbelin | 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. | Théo Zimmermann | 2018-06-27 |
| | | | | |||
* | | | | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | 2018-06-27 |
|\ \ \ \ | |_|/ / |/| | | | |||
* | | | | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | Pierre-Marie Pédrot | 2018-06-26 |
|\ \ \ \ | | | | | | | | | | | | | | | | constants | ||
* \ \ \ \ | Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵ | Maxime Dénès | 2018-06-26 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | build | ||
* \ \ \ \ \ | Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things. | Maxime Dénès | 2018-06-26 |
|\ \ \ \ \ \ | |||
| | | | * | | | Add overlay for elpi | Gaëtan Gilbert | 2018-06-26 |
| | | | | | | | |||
| | | | * | | | Remove Sorts.contents | Gaëtan Gilbert | 2018-06-26 |
| |_|_|/ / / |/| | | | | | |||
| | | * | | | Add overlay for Equations, Elpi | Gaëtan Gilbert | 2018-06-26 |
| | | | | | | |||
| | * | | | | Activate the build of Ltac2 and Equations in the Windows installer. | Théo Zimmermann | 2018-06-25 |
| | | | | | | |||
| | * | | | | Reuse CI info to know which version of plugins to build on Windows. | Théo Zimmermann | 2018-06-25 |
| | | | | | | |||
| | * | | | | Fix for issue 7707: include Ltac2 and Equations in Windows build | Michael Soegtrop | 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. | Hugo Herbelin | 2018-06-25 |
| |_|_|/ |/| | | | |||
| | | * | Critical bugs: added #3243 and Gonthier's bug in lazy machine. | Hugo Herbelin | 2018-06-25 |
| |_|/ |/| | | | | | | | | Both reminded by Enrico. | ||
* | | | Merge PR #7895: Revert "Add a note about [ci skip] in CI README." | Emilio Jesus Gallego Arias | 2018-06-24 |
|\ \ \ | |||
* \ \ \ | Merge PR #7805: Towards listing the critical bugs of the history of Coq. | Théo Zimmermann | 2018-06-24 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #7893: Update dpdgraph branch name | Théo Zimmermann | 2018-06-22 |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
| | | * | | Revert "Add a note about [ci skip] in CI README." | Théo Zimmermann | 2018-06-22 |
| |_|/ / |/| | | | | | | | | | | | This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d. | ||
| | | * | Fix Windows install script following removal of INSTALL.ide and move of ↵ | Théo Zimmermann | 2018-06-22 |
| |_|/ |/| | | | | | | | | INSTALL.doc. | ||
* | | | Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3 | Maxime Dénès | 2018-06-21 |
|\ \ \ | |||
| | * | | Update dpdgraph branch name | Gaëtan Gilbert | 2018-06-21 |
| |/ / |/| | | | | | | | | See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context | ||
* | | | Merge PR #7797: Remove reference name type. | Enrico Tassi | 2018-06-19 |
|\ \ \ | |||
| * | | | Overlay for reference removal | Maxime Dénès | 2018-06-18 |
| | | | | |||
* | | | | Update section on adding your project to CI and link to example PR. | Théo Zimmermann | 2018-06-18 |
| | | | | |||
| * | | | Remove reference name type. | Maxime Dénès | 2018-06-18 |
|/ / / | | | | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. | ||
* | | | Merge PR #7752: [merge script] Check if the CI that was run is outdated. | Maxime Dénès | 2018-06-17 |
|\ \ \ | |||
| | | * | Very first try at listing the critical bugs of the history of Coq. | Hugo Herbelin | 2018-06-15 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I let open several questions about fixes to the kernel which maybe were not critical. I skipped what seemed to have been bugs in beta-releases. Need double-checks, decision about the format, etc. | ||
* | | | | Merge PR #7793: [ci] update docker image to include elpi 1.0.4 | Emilio Jesus Gallego Arias | 2018-06-14 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵ | Matthieu Sozeau | 2018-06-14 |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | | | | | | to anomaly) | ||
| | * | | | [ci] update docker image to include elpi 1.0.4 | Enrico Tassi | 2018-06-13 |
| | | | | | |||
* | | | | | Document how to restart failed CI jobs. | Théo Zimmermann | 2018-06-13 |
| | | | | | | | | | | | | | | | | | | | | [ci skip] | ||
* | | | | | Markdown docs: switch from absolute to relative links. | Théo Zimmermann | 2018-06-13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip] |