coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| * \| \|	[doc] Fix an incorrect use of $PWD in Makefile.doc	Clément Pit-Claudel	2018-05-22
\| \| \| \| \| \| \| \| \| \| * \| \|	[doc] Add a setting to warn about empty Coq objects	Clément Pit-Claudel	2018-05-22
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Add myself as a secondary maintainer for the documentation.	Théo Zimmermann	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[build] Add -cclib -lcoqrun options to build of kernel.cmxa.	Emilio Jesus Gallego Arias	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
\|/ / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| * \|	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
\| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \|	[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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \