coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Printing goals does not evar-normalizes beforehand anymore.	Pierre-Marie Pédrot	2017-08-01
*	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
*	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès	2017-08-01
\|\
* \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| *	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\|/
*	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès	2017-07-19
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
* \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
* \|	Add printing of cumulativity in inductive types	Amin Timany	2017-06-16
* \|	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| *	[proof] Move bullets to their own module.	Emilio Jesus Gallego Arias	2017-06-12
* \|	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
\|/
*	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias	2017-06-01
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\| \|\
\| \| *	Simplified compaction criterion + tests.	Pierre Courtieu	2017-05-16
\| \| *	Adapted to EConstr.	Pierre Courtieu	2017-05-05
\| * \|	Warning removed.	Pierre Courtieu	2017-05-04
\| * \|	labelizing arguments	Pierre Courtieu	2017-05-04
\| * \|	Adding an option "Printing Unfocused".	Pierre Courtieu	2017-05-04
\| \| *	Adding an even more compact mode for goal display.	Pierre Courtieu	2017-05-03
\| \|/
\| *	Remove some unused values and types	Gaetan Gilbert	2017-04-27
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\
\| *	[flags] Documentation and a minor tweak.	Emilio Jesus Gallego Arias	2017-04-12
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\\|
\| *	[pp] Prepare for serialization, remove opaque glue.	Emilio Jesus Gallego Arias	2017-03-21
\| *	Fixing Bug 5383 (Hyps Limit) + small refactoring.	Pierre Courtieu	2017-03-07
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Moving printing code from Evd to Termops.	Pierre-Marie Pédrot	2017-02-14
* \|	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Tactic_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Goal API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|/\|
\| *	Do not print dependent evars by default (expensive)	Matthieu Sozeau	2016-11-05
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\|
\| *	Refine printing of pending unification constraints	Matthieu Sozeau	2016-10-20
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\|
\| *	Moving "move" in the new proof engine.	Hugo Herbelin	2016-09-24
* \|	CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...	Matej Kosik	2016-08-26
* \|	CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"	Matej Kosik	2016-08-26
* \|	CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"	Matej Kosik	2016-08-26