coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| * \|	fixed typo for assert_suceed	charguer	2018-07-10
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	[travis] Try to workaround the repeated APT failures by using Jason Gross's ↵	Théo Zimmermann	2018-07-10
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	suggestion.
\| * / / / /	Remove auto-retry in GitLab CI now that @coqbot is handling it.	Théo Zimmermann	2018-07-10
\|/ / / / /
* \| \| \| \|	Merge PR #7899: My recent improvements to the backport script.	Maxime Dénès	2018-07-10
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.	Maxime Dénès	2018-07-10
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #8028: Fix a few typos	Théo Zimmermann	2018-07-10
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #8025: Fix rst syntax for `quote ident {ident}`	Théo Zimmermann	2018-07-10
\|\ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \|	Add new options --no-conflict and --no-signature-check to backport script.	Théo Zimmermann	2018-07-10
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Fix typo in doc/proof-engine/tactics.rst.	whitequark	2018-07-10
\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Fix typo in Init.Logic.	whitequark	2018-07-10
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7920: Generic syntax for attributes	Maxime Dénès	2018-07-09
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	Fix rst syntax for `quote ident {ident}`	Joachim Breitner	2018-07-09
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.	Matthieu Sozeau	2018-07-09
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Introduce a team of code owners for the CI system.	Théo Zimmermann	2018-07-09
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This means that all the members of the team will receive a review request for PRs on the CI, but only one of them will need to approve the PR, and this will remove the review request for the others. Currently the team contains Emilio and Gaetan, the two former code owners of these files. It makes sense to start experimenting on this component since they had already decided to make their role symmetric. Updating the list of maintainers can be done by updating the list members, and without changing the CODEOWNER file.
* \| \| \| \| \| \|	Merge PR #8015: Output UTF-8 explicitly in timing tools	Jason Gross	2018-07-08
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Get rid of horrendous hack limiting the size of parsed integers	Maxime Dénès	2018-07-08
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7985: Remove letouzey from CODEOWNERS since he left the Coq ↵	Maxime Dénès	2018-07-08
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	organization.
* \ \ \ \ \ \ \	Merge PR #8020: Modify URLs in xml-protocol.md	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-08
\|/ / / / / / / /
* \| \| \| \| \| \| \|	Merge PR #7843: Remove Emacs modes	Maxime Dénès	2018-07-08
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Mention the removal of Emacs modes in CHANGES.	Théo Zimmermann	2018-07-08
\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Remove Emacs modes.	Théo Zimmermann	2018-07-08
\|/ / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead.
\| \| \| \| \| \| \| *	make diff sort by difference, not absolute difference	Ralf Jung	2018-07-07
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	make-both-single-timing-files: fix --sort-by=diff	Ralf Jung	2018-07-07
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	Output UTF-8 explicitly in timing tools	Jasper Hugunin	2018-07-07
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7921: Archive the `gallina` tool	Maxime Dénès	2018-07-07
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Add an overlay.	Pierre-Marie Pédrot	2018-07-07
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7956: Rebuild coqtop$(EXE) in "make coqbinaries" in addition to ↵	Enrico Tassi	2018-07-07
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coqtop.opt$(EXE).
\| \| \| \| \| \| \| \| *	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.
\| \| \| \| \| \| \| \| *	Remove dead code that used to be there for CamlpX compatibility.	Pierre-Marie Pédrot	2018-07-07
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Part of this code has been introduced very recently in 7c62654 in spite of the existence of a proper API. This means that this should be better documented.
* \| \| \| \| \| \| \|	Merge PR #8005: Fix compilation of Coq with camlp5 master branch.	Emilio Jesus Gallego Arias	2018-07-07
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #8001: Cache the build of the Nix package using Cachix.	Gaëtan Gilbert	2018-07-06
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7821: [refine] obey the use_unification_heuristics flag	Pierre-Marie Pédrot	2018-07-06
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #8008: Add test for #8004.	Théo Zimmermann	2018-07-06
\|\ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \|	[pkg:nix] Add more comments and allow overriding extra substituters.	Théo Zimmermann	2018-07-06
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Add test for #8004.	Gaëtan Gilbert	2018-07-06
\|/ / / / / / / / / /
\| \| \| * / / / / / /	Fix compilation of Coq with camlp5 master branch.	Pierre-Marie Pédrot	2018-07-06
\| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There was a conflict in the name of an exported function. A good argument in favour of PR #7898.
* \| \| \| \| \| \| \| \|	Merge PR #7990: Convert timing tool to python3	Jason Gross	2018-07-05
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	refine: obey the use_unification_heuristics flag	Matthieu Sozeau	2018-07-05
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7991: Make Travis faster by removing more builds.	Emilio Jesus Gallego Arias	2018-07-05
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7994: Make bin/ in makefile, not configure.	Emilio Jesus Gallego Arias	2018-07-05
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \|	[pkg:nix] Stop using lib.inNixShell.	Théo Zimmermann	2018-07-05
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	[pkg:nix] Change the download method.	Théo Zimmermann	2018-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will allow for better reuse of the cache when the URL is different but the archive is the same.
\| \| \| \| * \| \| \| \| \| \|	[pkg:nix] Pass through the ocamlPackages version used to build.	Théo Zimmermann	2018-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will be useful for users wanting to build a plugin using this package.
\| \| \| \| * \| \| \| \| \| \|	[pkg:nix] Cache the build using Cachix when signing key is set.	Théo Zimmermann	2018-07-05
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \|	Remove some Travis jobs to make the build faster.	Théo Zimmermann	2018-07-05
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	Turn a dead branch into an assertion failure in VM reification.	Pierre-Marie Pédrot	2018-07-05
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In #7607, dead code that used to handle non-dependent return predicates was removed. This made the reification branch expecting non-functions in predicates dead code. We fix this by using an assert instead.
* \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \