coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move solve_constraint_system near its only use site (comInductive)	Gaëtan Gilbert	2018-05-17
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
*	Stop using Universes.subst(_opt)_univs_constr	Gaëtan Gilbert	2018-05-17
*	Make set minimization option internal to Universes	Gaëtan Gilbert	2018-05-17
*	Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...	Emilio Jesus Gallego Arias	2018-05-17
\|\
* \	Merge PR #7359: Reduce usage of evar_map references	Pierre-Marie Pédrot	2018-05-17
\|\ \
* \ \	Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...	Pierre-Marie Pédrot	2018-05-17
\|\ \ \
* \ \ \	Merge PR #6870: [ide] Don't set `quiet` on start.	Enrico Tassi	2018-05-17
\|\ \ \ \
* \ \ \ \	Merge PR #7525: [ci] Try to build more of fiat-crypto.	Gaëtan Gilbert	2018-05-17
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6808: Add unit tests to test-suite	Gaëtan Gilbert	2018-05-17
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Document nested proofs and associated option.	Théo Zimmermann	2018-05-17
\| \| \| \| \| \| *	[STM] Nested Proofs Allowed has to be executed immediately	Enrico Tassi	2018-05-17
\| \| \| \| \| \| *	Remove deprecation warning for nested proofs.	Théo Zimmermann	2018-05-17
\| \| \| \| \| \| *	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.	Maxime Dénès	2018-05-16
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Modify make system to include Makefile.common in the test suite	Gaëtan Gilbert	2018-05-16
\| \| \| * \| \| \|	[ci] Try to build more of fiat-crypto.	Emilio Jesus Gallego Arias	2018-05-16
\| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7514: [ci] Don't build lite versions of CI developments.	Gaëtan Gilbert	2018-05-16
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7535: Typo in documentation of Derive	Théo Zimmermann	2018-05-16
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7493: Minor update of the documentation about the rcfile	Emilio Jesus Gallego Arias	2018-05-16
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	Typo in documentation of Derive	Joachim Breitner	2018-05-16
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7079: Remove naked pointers from the VM	Maxime Dénès	2018-05-16
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7391: Add a small documentation writer's guide	Maxime Dénès	2018-05-16
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	unit tests: add .merlin	Gaëtan Gilbert	2018-05-16
\| \| \| \| \| \| * \| \| \|	add unit tests to test suite	Paul Steckler	2018-05-16
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7436: [travis] Remove some more jobs from PR testing now that they ...	Gaëtan Gilbert	2018-05-16
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	Minor update of the documentation/man about the resource file.	Hugo Herbelin	2018-05-16
* \| \| \| \| \| \| \| \| \|	Merge PR #7484: Fix non-portable shebang in test-suite.	Enrico Tassi	2018-05-16
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7227: [ssr] import ssreflect test suite from math-comp	Maxime Dénès	2018-05-16
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7442: Gitlab: build docker image in pipeline and use through registry.	Emilio Jesus Gallego Arias	2018-05-16
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \|	[ci] Don't build lite versions of CI developments.	Emilio Jesus Gallego Arias	2018-05-16
\| \| \| \| * \| \| \| \| \| \| \| \|	[travis] Remove some more jobs from PR testing now that they are on Gitlab.	Emilio Jesus Gallego Arias	2018-05-16
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \|	[ide] Don't set `quiet` on start.	Emilio Jesus Gallego Arias	2018-05-16
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7507: gitlab CI: fix [warnings] template	Emilio Jesus Gallego Arias	2018-05-16
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7505: Pick up user overlays when running GitLab CI on PRs.	Emilio Jesus Gallego Arias	2018-05-16
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7519: git / gpg integration link	Théo Zimmermann	2018-05-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7465: Don't use ref universe_opt_subst in universe normalisation fu...	Pierre-Marie Pédrot	2018-05-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] More feedback on doc writer guide	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Search for 'coqtop' in $PATH if COQBIN is unset	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Address feedback on doc writer guide	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Clarify a comment in the README	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Add an ELisp snippet to insert Sphinx roles and quotes	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Add a README to doc/sphinx/	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Document all directives and roles of our Sphinx domain	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Small fixes	Clément Pit-Claudel	2018-05-15
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[doc] Compute the path to coqdoc at run time, not at load time	Clément Pit-Claudel	2018-05-15
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Update MERGING.md	Matthieu Sozeau	2018-05-15
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Update MERGING.md	Matthieu Sozeau	2018-05-15
\| \| * \| \| \| \| \| \| \| \| \| \| \|	git / gpg integration link	Matthieu Sozeau	2018-05-15
\| \| \| \|_\|_\|_\|_\|_\|_\|/ / / / \| \| \|/\| \| \| \| \| \| \| \| \| \|