coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| * \|	Glob_ops: cosmetic renaming to reflect the type of objects.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR #7090: stm: don't propagate side effects when editing a proof	Emilio Jesus Gallego Arias	2018-03-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6961: [test-suite] Add backtracking test for `Load`.	Enrico Tassi	2018-03-28
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	stm: don't propagate side effects when editing a proof	Enrico Tassi	2018-03-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Adding tacticals tclBINDFIRST/tclBINDLAST.	Hugo Herbelin	2018-03-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Design choice: Failing with an anomaly or with a catchable Ltac error "Fail": we fail with a Fail as it was the case with the related constrained version of tclTHENFIRST/tclTHENLAST.
\| \| \| \| \| \| \| *	Export Proofview.undefined as "unsafe" primitive.	Hugo Herbelin	2018-03-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Adding informative variant of shelve_unifiable returning set of shelved evars.	Hugo Herbelin	2018-03-27
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *"	Pierre-Marie Pédrot	2018-03-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7062: Slightly refining some error messages about unresolvable evars.	Pierre-Marie Pédrot	2018-03-27
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	[doc] Port Chapter 20 Type Classes to Sphinx	Matthieu Sozeau	2018-03-26
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵	Maxime Dénès	2018-03-26
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	AppVeyor fail.
\| \| \| \| \| \| * \| \|	Move Classes.tex to type-classes.rst	Matthieu Sozeau	2018-03-26
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.	Enrico Tassi	2018-03-26
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Add Michael Soegtrop as a code owner for Windows build scripts.	Théo Zimmermann	2018-03-26
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Use Pierre Corbineau GitHub nickname in CODEOWNERS.	Théo Zimmermann	2018-03-26
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\| \|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For instance, error in "Goal forall a f, f a = 0" is now located.
\| \| \| * \| \| \|	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
\| \|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- The case 0 makes the code of intros until (and in particular of Detyping.lookup_quantified_hypothesis_as_displayed more complicated). - The introduction pattern "*" is compositional while "until 0" is not.
* \| \| \| \| \|	Merge PR #7046: Switch maintainers for documentation	Théo Zimmermann	2018-03-23
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7018: Fix typo in CHANGES.	Maxime Dénès	2018-03-23
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7029: improve merge-pr script	Maxime Dénès	2018-03-23
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	improve merge-pr script	Enrico Tassi	2018-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The script now performs many more checks and reports errors in a more intelligible way.
* \| \| \| \| \| \| \| \|	Merge PR #7052: More precise wording about the merge process.	Théo Zimmermann	2018-03-23
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	More precise wording about the merge process.	Maxime Dénès	2018-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.
* \| \| \| \| \| \| \| \|	Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ↵	Enrico Tassi	2018-03-23
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	too long.
* \ \ \ \ \ \ \ \ \	Merge PR #6968: [stm] Never consider `Backtrack` as part of the script.	Enrico Tassi	2018-03-23
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7025: Coq makefile: provide variables to extend the flags passed ↵	Enrico Tassi	2018-03-23
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to coq, coqchk, coqdoc
\| * \| \| \| \| \| \| \| \| \| \|	update CHANGES	Enrico Tassi	2018-03-23
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7030: [default.nix] Add dependencies of the merging script.	Vincent Laporte	2018-03-23
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7031: Owners for developer tools	Théo Zimmermann	2018-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	Owners for developer tools	Maxime Dénès	2018-03-22
\|/ / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \|	Merge pull request #7040 from maximedenes/sphinx-doc-chapter-22	Guillaume Melquiond	2018-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sphinx doc chapter 22
\| * \ \ \ \ \ \ \ \ \ \ \	Merge branch 'master' into sphinx-doc-chapter-22	Guillaume Melquiond	2018-03-22
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge pull request #7039 from maximedenes/sphinx-doc-chapter-21	Guillaume Melquiond	2018-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sphinx doc chapter 21
\| * \ \ \ \ \ \ \ \ \ \ \ \	Merge branch 'master' into sphinx-doc-chapter-21	Guillaume Melquiond	2018-03-22
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge pull request #7038 from maximedenes/sphinx-doc-chapter-19	Guillaume Melquiond	2018-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sphinx doc chapter 19
\| * \ \ \ \ \ \ \ \ \ \ \ \ \	Merge branch 'master' into sphinx-doc-chapter-19	Guillaume Melquiond	2018-03-22
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge pull request #7036 from maximedenes/sphinx-doc-chapter-17	Guillaume Melquiond	2018-03-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Sphinx doc chapter 17
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Switch maintainers for documentation	Maxime Dénès	2018-03-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Guillaume and I agreed to switch, as the new Sphinx infrastructure changes this component significantly.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Add chapter 22	Maxime Dénès	2018-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Paul Steckler for porting this chapter.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Move chapter 22 to new infrastructure	Maxime Dénès	2018-03-22
\| \|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Add chapter 21	Maxime Dénès	2018-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Pierre Letouzey for porting this chapter.
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Move chapter 21 to new infrastructure	Maxime Dénès	2018-03-22
\| \|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Add chapter 19	Maxime Dénès	2018-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Laurent Théry for porting this chapter.
\| \| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Move chapter 19 to new infrastructure	Maxime Dénès	2018-03-22
\| \|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Add chapter 17	Maxime Dénès	2018-03-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Clément Pit-Claudel for porting this chapter.
\| * \| \| \| \| \| \| \| \| \| \|	[Sphinx] Move chapter 17 to new infrastructure	Maxime Dénès	2018-03-22
\|/ / / / / / / / / / /
\| \| * \| \| \| \| \| \| \| \|	docs	Ralf Jung	2018-03-21
\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	[default.nix] Add dependencies of the merging script.	Théo Zimmermann	2018-03-21
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7027: Refine a bit the decentralized merging process.	Théo Zimmermann	2018-03-21
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Switching owners for `META.coq`	Maxime Dénès	2018-03-21
\| \| \| \| \| \| \| \| \| \|