coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
* \| \|	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
* \| \| \|	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\| \| \| *	[cleanup] Change Id.t option to Name.t in TacFun	Tej Chajed	2017-02-16
\| \|_\|/ \|/\| \|
* \| \|	Merge PR#393: Replace Typeops with Fast_typeops	Maxime Dénès	2017-02-08
\|\ \ \
* \| \| \|	Revert "Extraction: avoid deprecated functions of module String"	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction cosmetic: no whitespaces in printing empty modules	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction: avoid deprecated functions of module String	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction: simplify the generated code for difficult name conflicts	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction : get_duplicates (via option) instead of check_duplicates (via Not...	Pierre Letouzey	2017-02-07
* \| \| \|	Extraction: fix complexity issue #5310	Pierre Letouzey	2017-02-07
\| \|_\|/ \|/\| \|
\| \| *	Extraction: fix complexity issue #5310	Pierre Letouzey	2017-02-07
\| * \|	Remove useless comments	Gaetan Gilbert	2017-01-28
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\ \ \ \| \| \|/ \| \|/\|
\| \| *	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\| \|/ \|/\|
\| *	ssrmatching: fix iter_constr_LR iterator wrt Proj	Enrico Tassi	2016-12-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|\\|
\| *	ssrmatching: handle primite projections (fix: #5247)	Enrico Tassi	2016-12-05
\| *	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-12-02
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\|
\| *	Lazily load constants in micromega (bug #5134).	Guillaume Melquiond	2016-11-24
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\| \|\
* \| \|	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\| \|
\| * \|	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \
\| * \ \	Merge commit 'a799600' into v8.6	Maxime Dénès	2016-10-25
\| \|\ \ \
\| \| * \| \|	That Function is unable to create a Fixpoint equation is a user problem,	Yves Bertot	2016-10-25
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \| \|
\| * \| \| \|	ssrmatching: fix interpretation of rpattern	Enrico Tassi	2016-10-24
\| \|/ / /