coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \
\| \| \| *	Fixing a bug of Print for inductive types with let-ins in parameters.	Hugo Herbelin	2017-12-14
* \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \|_\|/ \|/\| \|
\| * \|	Catch errors while coercing 'and' intro patterns	Tej Chajed	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
\|\ \ \
* \ \ \	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
\| \|_\|/ / / / \|/\| \| \| \| \|
\| * \| \| \| \|	more complete not-fully-applied error messages, #6145	Paul Steckler	2017-11-28
\| \| \| \| \| *	Make the micromega extraction check a regular output test.	Gaëtan Gilbert	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
* \| \| \| \|	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
* \| \| \| \|	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
* \| \| \| \|	Fix defining non primitive projections with abstracted universes.	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
\| \|_\|/ \|/\| \|
\| \| *	allow whitespace around infix op	Paul Steckler	2017-11-22
\| \| *	use OCaml criteria for infix ops, #6212	Paul Steckler	2017-11-22
\| \|/ \|/\|
* \|	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-20
\|/
*	Binding ltac printing functions to the system of generic printing.	Hugo Herbelin	2017-11-02
*	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann	2017-10-19
*	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert	2017-10-10
*	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
*	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...	Maxime Dénès	2017-10-09
\|\
* \	Merge PR #1078: Report missing arguments in error message	Maxime Dénès	2017-10-04
\|\ \
* \ \	Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).	Maxime Dénès	2017-10-04
\|\ \ \
\| \| \| *	BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations	Paul Steckler	2017-09-25
\| \| * \|	Report missing arguments in error message	Tej Chajed	2017-09-21
\| \| \|/
\| * /	Fixing bug #5741 (anomaly in info_trivial).	Hugo Herbelin	2017-09-19
\| \|/
* /	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\|/
*	Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...	Maxime Dénès	2017-09-15
\|\
* \|	Fixing bug #5693 (treating empty notation format as any format).	Hugo Herbelin	2017-09-12
* \|	Fixing a bug of recursive notations introduced in dfdaf4de.	Hugo Herbelin	2017-09-12
* \|	Adding a test for #5569 (warning about skipping spaces).	Hugo Herbelin	2017-08-29
* \|	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
\| *	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
\|/
*	Print names of all open blocks	Tej Chajed	2017-08-06
*	Merge PR #834: Adding support for recursive notations of the form "x , .. , y...	Maxime Dénès	2017-08-01
\|\
* \|	Fix TypeclassDebug.out after conflicting PR merges	Matthieu Sozeau	2017-07-26
\| *	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/
*	Merge PR #869: Enforce alternating separators in typeclass debug output	Maxime Dénès	2017-07-20
\|\