coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\| * \|	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| \|/
\| *	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
\| * \|	Merge PR#454: Printing unfocussed goals and toward a pg plugin.	Maxime Dénès	2017-05-05
\| \|\ \
\| \| \| *	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
\| \| \|/
\| * /	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
\| \|/
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\| \|\ \
\| \| \| *	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| \| \| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \| \| *	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| \| \|/ \| \|/\|
* \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] More located use.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[constrexpr] Make patterns use Loc.located for location information	Emilio Jesus Gallego Arias	2017-04-24
\|/ /
* \|	Merge PR#552: Miscelaneous commits	Maxime Dénès	2017-04-24
\|\ \
* \| \|	Remove VernacError	Gaetan Gilbert	2017-04-21
\| * \|	refactoring "Ppvernac.pr_extend"	Matej Kosik	2017-04-20
\|/ /
* \|	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
\| \| *	Removing internal support for accepting "{struct x}" and co in "Theorem with".	Hugo Herbelin	2017-04-09
\| \|/
* \|	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
\| \|\
\| * \|	Fix higher-order pattern variables not being printed as "@?" (bug #5431).	Guillaume Melquiond	2017-04-02
\| * \|	Merge PR#511: [stm] Remove some obsolete vernacs/classification.	Maxime Dénès	2017-03-30
\| \|\ \
\| * \| \|	Do so that "About" tells if a reference is a coercion.	Hugo Herbelin	2017-03-27
* \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\\| \| \|
\| \| * \|	[stm] Remove some obsolete vernacs/classification.	Emilio Jesus Gallego Arias	2017-03-24
\| \|/ /
\| \| *	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin	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
\| \|/
\| *	[pp] Move terminal-specific tagging to the toplevel.	Emilio Jesus Gallego Arias	2017-03-21
\| *	[pp] Prepare for serialization, remove opaque glue.	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
\| *	Attempt to improve error message when "apply in" fail.	Hugo Herbelin	2017-03-15
\| *	Fixing Bug 5383 (Hyps Limit) + small refactoring.	Pierre Courtieu	2017-03-07