coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Maitainers for components of the test-suite (closes #7426).	Théo Zimmermann	2018-05-20
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[codeowner] Add comment.	Théo Zimmermann	2018-05-20
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Make Pierre-Marie a secondary maintainer of the kernel and checker.	Théo Zimmermann	2018-05-20
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7557: Add test cases from #7554	Théo Zimmermann	2018-05-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add test cases from #7554	Tej Chajed	2018-05-20
\| \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging...	Michael Soegtrop	2018-05-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7550: [CI] Fix the script used by math-classes.	Emilio Jesus Gallego Arias	2018-05-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Clean-up dead file in test-suite.	Théo Zimmermann	2018-05-18
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Create a documentation for the release manager.	Théo Zimmermann	2018-05-18
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	[CI] Fix the script used by math-classes.	Pierre-Marie Pédrot	2018-05-18
\| \|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Split off Universes functions for minimization.	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Make Universes.refresh_constraints internal to UState	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Remove unused argument to solve_constraints_system	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \|	[circle] Use Docker image from Gitlab registry.	Emilio Jesus Gallego Arias	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
\| \|/ / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[sphinx] Bump timeout. Closes #7532.	Clément Pit-Claudel	2018-05-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[sphinx] Fix mistake in index.	Théo Zimmermann	2018-05-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[sphinx] Improve rewrite section in tactic chapter.	Théo Zimmermann	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[windows] Don't make menhir and int anymore.	Emilio Jesus Gallego Arias	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[ssr] fix after to_constr ~abort_on_undefined_evars was added	Enrico Tassi	2018-05-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7484: Fix non-portable shebang in test-suite.	Enrico Tassi	2018-05-16
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \