coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Using name given by user to name a 'pat, if any.	Hugo Herbelin	2018-02-20
* \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
* \|	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin	2018-02-20
\|/
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \
\| * \|	More detailed error messages for Canonical Structure, #6398	Paul Steckler	2018-02-06
* \| \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
* \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
* \|	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\ \
* \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
* \| \|	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
\|\