coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7567: Clean-up dead file in test-suite.	Enrico Tassi	2018-05-23
\|\
* \	Merge PR #7565: Document the new nested-proof error message.	Emilio Jesus Gallego Arias	2018-05-22
\|\ \
* \ \	Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before lib.c...	Emilio Jesus Gallego Arias	2018-05-22
\|\ \ \
\| * \| \|	Fixing debugger after #6859 (loading dynlink.cma before lib.cma).	Hugo Herbelin	2018-05-22
* \| \| \|	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\ \ \ \ \| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7324: Infrastructure for ocamldebug on the checker	Hugo Herbelin	2018-05-22
\|\ \ \ \
* \ \ \ \	Merge PR #7526: [circle] Use Docker image from Gitlab registry.	Gaëtan Gilbert	2018-05-22
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span mu...	Gaëtan Gilbert	2018-05-22
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6859: [stm] Make toplevels standalone executables.	Théo Zimmermann	2018-05-22
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	[ci] [gitlab] Fix printenv sorting for variables that span multiple lines.	Emilio Jesus Gallego Arias	2018-05-21
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Document the new nested-proof error message.	Théo Zimmermann	2018-05-21
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| * \| \| \| \|	[ide] Remove special option `-ideslave`	Emilio Jesus Gallego Arias	2018-05-21
\| * \| \| \| \|	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias	2018-05-21
\| * \| \| \| \|	[ci] Add Dune to the base system.	Emilio Jesus Gallego Arias	2018-05-21
\|/ / / / /
* \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	[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
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \