coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix an unhandled exception in Omega.	Pierre-Marie Pédrot	2017-04-07
*	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\
\| *	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\| \|\
\| * \	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\| \|\ \
* \| \| \|	Fix a normalization hotspot in computation of constr keys.	Pierre-Marie Pédrot	2017-04-06
* \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\\| \| \|
\| * \| \|	Merge PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\| \|\ \ \
* \| \| \| \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| * \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
* \| \| \| \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \| \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\\| \| \| \|
\| \| * \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \| * \| \|	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
\| \| * \| \|	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
\| \| * \| \|	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
\| \|/ / /
\| * \| \|	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès	2017-03-23
\| * \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\| \|\ \ \
\| \| * \ \	Merge PR#495: funind: Ignore missing info for current function	Maxime Dénès	2017-03-23
\| \| \|\ \ \
\| \| \| \| * \|	Fast path for implicit tactic solving.	Pierre-Marie Pédrot	2017-03-23
\| \| \| \| * \|	Ensuring static invariants about handling of pending evars in Pretyping.	Pierre-Marie Pédrot	2017-03-23
\| \| * \| \| \|	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| * \| \| \| \|	Mark ring morphisms as opaque.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \|	Fix broken evaluation strategies for ring and field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \|	Remove duplicate lemmas.	Guillaume Melquiond	2017-03-22
\| \| \|_\|/ / \| \|/\| \| \|
\| \| \| * \|	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\| \| \|/ /
\| * \| \|	[extraction] Flush formatters at end of output.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Move terminal-specific tagging to the toplevel.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Make feedback the only logging mechanism.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Force well-formed boxes by construction.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Prepare for serialization, remove opaque glue.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Remove `Pp.stras`.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias	2017-03-21
\| * \| \|	Merge PR#134: Enable `-safe-string`	Maxime Dénès	2017-03-21
\| \|\ \ \
\| * \ \ \	Merge PR#428: Report missing tactic arguments in error message	Maxime Dénès	2017-03-17
\| \|\ \ \ \
\| * \ \ \ \	Merge PR#445: TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès	2017-03-17
\| \|\ \ \ \ \
\| * \| \| \| \| \|	Attempt to improve error message when "apply in" fail.	Hugo Herbelin	2017-03-15
\| \| \| \| * \| \|	[safe-string] plugins/extraction	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| * \| \|	[safe-string] ltac/profile_ltac	Emilio Jesus Gallego Arias	2017-03-14
\| \| \|_\|/ / / \| \|/\| \| \| \|
\| \| \| * \| \|	Report missing tactic arguments in error message	Tej Chajed	2017-03-14
\| \| \|/ / / \| \|/\| \| \|
\| * \| \| \|	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès	2017-03-14
\| \|\ \ \ \
\| * \| \| \| \|	Micromega: removing a constant preventing micromega to be loaded before Logic.v.	Hugo Herbelin	2017-03-09
\| \| \| \| \| *	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \| \|_\|_\|/ \| \|/\| \| \|
\| \| \| \| *	[ltac] Move dummy plugin to plugins folder.	Emilio Jesus Gallego Arias	2017-03-03
\| * \| \| \|	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès	2017-02-27
\| \|\ \ \ \
\| \| \| \| * \|	TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès	2017-02-24
\| \| \|_\|/ / \| \|/\| \| \|
\| * \| \| \|	Revert "Add empty ltac_plugin file for forward compatibility."	Maxime Dénès	2017-02-24
\| * \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-22
\| \|\ \ \ \ \| \| \| \|_\|/ \| \| \|/\| \|
\| * \| \| \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17