aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-07-08Modify URLs in xml-protocol.mdRin Arakaki
2018-07-07Add an overlay.Pierre-Marie Pédrot
2018-07-07Introduce 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-05Merge PR #7746: Many small cleanups removing unused arguments and functionsPierre-Marie Pédrot
2018-07-05Merge PR #7979: TACTIC EXTEND in coqppEmilio Jesus Gallego Arias
2018-07-04[ci] Avoid annoying detached head warning.Emilio Jesus Gallego Arias
2018-07-03Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵Gaëtan Gilbert
with apt.
2018-07-03Add overlay for equations.Gaëtan Gilbert
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-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-02Documenting the syntax changes.Pierre-Marie Pédrot
2018-07-02Add Equations overlayMatthieu Sozeau
2018-07-02Clean 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-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Emilio Jesus Gallego Arias
points of Camlp5
2018-07-01Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵Emilio Jesus Gallego Arias
.git anymore.
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Emilio Jesus Gallego Arias
Z into three files
2018-06-29Adding an overlay for the PR.Pierre-Marie Pédrot
2018-06-29Documenting the transition strategy of GEXTEND.Pierre-Marie Pédrot
2018-06-29Document that GITURL variables shouldn't have a trailing .git anymore.Théo Zimmermann
This allows to append /archive at the end.
2018-06-29Merge PR #7918: Mini-update of version history with recent changes.Théo Zimmermann
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Maxime Dénès
constr in Constr
2018-06-29Merge PR #7745: Make type Environ.globals abstract + simplify ↵Maxime Dénès
Environ.retroknowledge
2018-06-28Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.Michael Soegtrop
2018-06-28Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.Théo Zimmermann
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
2018-06-27Adding overlay.Hugo Herbelin
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
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).
2018-06-27Fix 'unbound variable' issue on Windows packaging jobs.Théo Zimmermann
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Pierre-Marie Pédrot
constants
2018-06-26Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵Maxime Dénès
build
2018-06-26Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Maxime Dénès
2018-06-26Add overlay for elpiGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-26Add overlay for Equations, ElpiGaëtan Gilbert
2018-06-25Activate the build of Ltac2 and Equations in the Windows installer.Théo Zimmermann
2018-06-25Reuse CI info to know which version of plugins to build on Windows.Théo Zimmermann
2018-06-25Fix for issue 7707: include Ltac2 and Equations in Windows buildMichael Soegtrop
On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
2018-06-25Mini-update of version history with recent changes.Hugo Herbelin
2018-06-25Critical bugs: added #3243 and Gonthier's bug in lazy machine.Hugo Herbelin
Both reminded by Enrico.
2018-06-24Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Emilio Jesus Gallego Arias
2018-06-24Merge PR #7805: Towards listing the critical bugs of the history of Coq.Théo Zimmermann
2018-06-22Merge PR #7893: Update dpdgraph branch nameThéo Zimmermann
2018-06-22Revert "Add a note about [ci skip] in CI README."Théo Zimmermann
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
2018-06-22Fix Windows install script following removal of INSTALL.ide and move of ↵Théo Zimmermann
INSTALL.doc.
2018-06-21Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Maxime Dénès
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 10:05:25 +0000