coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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-12
\| \|
* \|	[ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0	Emilio Jesus Gallego Arias	2018-07-11
\|/ \| \| \| \| \|	- 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.
*	Merge PR #7898: Remove camlp4 remains	Emilio Jesus Gallego Arias	2018-07-11
\|\
* \|	Add new options --no-conflict and --no-signature-check to backport script.	Théo Zimmermann	2018-07-10
\| \|
* \|	Modify URLs in xml-protocol.md	Rin Arakaki	2018-07-08
\| \|
* \|	Modify URLs in xml-protocol.md	Rin Arakaki	2018-07-08
\| \|
\| *	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	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	Pierre-Marie Pédrot	2018-07-05
\|\
* \	Merge PR #7979: TACTIC EXTEND in coqpp	Emilio Jesus Gallego Arias	2018-07-05
\|\ \
* \| \|	[ci] Avoid annoying detached head warning.	Emilio Jesus Gallego Arias	2018-07-04
\| \| \|
* \| \|	Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵	Gaëtan Gilbert	2018-07-03
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	with apt.
\| \| \| *	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-03
\|\ \ \
\| \| * \|	[ci] [docker] Make sure we don't install optional packages with apt.	Emilio Jesus Gallego Arias	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.	Pierre-Marie Pédrot	2018-07-02
\| \| \|/
\| * /	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
\|\ \ \ \