coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\
* \	Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.	Maxime Dénès	2017-12-13
\|\ \
\| \| *	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| * \|	Fix anomaly in [Type foo] command, + print uctx like Check.	Gaëtan Gilbert	2017-12-11
* \| \|	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\ \ \
\| \| \| *	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\ \ \
* \ \ \	Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).	Maxime Dénès	2017-12-05
\|\ \ \ \
* \ \ \ \	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès	2017-12-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6210: More complete not-fully-applied error messages, #6145	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Adding a test for #6304 (bug with fix in notations).	Hugo Herbelin	2017-12-03
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| * \| \|	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
\| \| \| * \| \|	Tests for global universe declarations	Matthieu Sozeau	2017-12-01
\| \| \| * \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	In injection/inversion, consider all template-polymorphic types as injectable.	Hugo Herbelin	2017-11-28
\| \| \| \| * \| \| \|	more complete not-fully-applied error messages, #6145	Paul Steckler	2017-11-28
\| \| * \| \| \| \| \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Selecting which notation to print based on current stack of scope.	Hugo Herbelin	2017-11-27
\| \| \| \| \| \| * \|	Pre-isolating a notation test to avoid interferences.	Hugo Herbelin	2017-11-27
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire...	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Fixing associativity registered for level 10.	Hugo Herbelin	2017-11-27
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Restrict universe context when declaring constants in obligations.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Fix #5347: unify declaration of axioms with and without bound univs.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Forbid repeated names in universe binders.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Universe binders survive sections, modules and compilation.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
\| \| \| \| * \| \| \|	In close_proof only check univ decls with the restricted context.	Gaëtan Gilbert	2017-11-24
\| \| \| \| * \| \| \|	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| \| \| \| * \| \| \|	restrict_universe_context: do not prune named universes.	Gaëtan Gilbert	2017-11-24
\| \| \| \| * \| \| \|	Fix defining non primitive projections with abstracted universes.	Gaëtan Gilbert	2017-11-24
\| \| \| \| * \| \| \|	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Printing again "intros **" as "intros" by default.	Hugo Herbelin	2017-11-24
\| \| \| \| \| \| *	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-24
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	coq_makefile tests: build in easily removed temporary subdirectory.	Gaëtan Gilbert	2017-11-24
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	Fixing failing mkdir in test-suite for coq-makefile.	Hugo Herbelin	2017-11-24
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6167: Fixing factorization of recursive notations with an atomic se...	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Recognizing Z in romega up to conversion.	Hugo Herbelin	2017-11-23