coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
*	Adding "epose", "eset", "eremember" which allow to set terms with	Hugo Herbelin	2017-05-30
*	Adding "eassert", "eenough", "epose proof", which allow to state	Hugo Herbelin	2017-05-30
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
* \	Merge PR#678: [coqlib] Move `Coqlib` to `library/`.	Maxime Dénès	2017-05-28
\|\ \
\| \| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
\| * \|	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
\| \|/
* /	Exporting a few primitive tacticals as named Ltac definitions.	Pierre-Marie Pédrot	2017-05-27
\|/
*	Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings	Maxime Dénès	2017-05-25
\|\
* \	Merge PR#608: Allow Ltac2 as a plugin	Maxime Dénès	2017-05-25
\|\ \
* \ \	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
\| \|/ / /
\| \| \| *	Using type classes in the interpretation of "specialize" and "contradiction".	Hugo Herbelin	2017-05-22
\| \| \| *	Clarifying the interpretation path for the "constr_with_binding" argument.	Hugo Herbelin	2017-05-22
\| \| \|/ \| \|/\|
\| \| *	Merge branch 'master' into ltac2-hooks	Pierre-Marie Pédrot	2017-05-19
\| \| \|\ \| \| \|/ \| \|/\|
\| * \|	Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.	Hugo Herbelin	2017-05-16
\| * \|	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
\| * \|	Merge PR#201: Transparent abstract	Maxime Dénès	2017-05-11
\| \|\ \
\| * \| \|	Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in bat...	Hugo Herbelin	2017-05-04
\| \| \| *	Generalizing the tactic-in-term embedding to any generic argument.	Pierre-Marie Pédrot	2017-05-03
\| \| \| *	Allowing to pass arbitrary data in internalization environments.	Pierre-Marie Pédrot	2017-05-03
\| \| \|/ \| \|/\|
\| * \|	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
\| * \|	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| * \|	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| * \|	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\| * \|	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\| * \|	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| * \|	Remove unused [rec] keywords	Gaetan Gilbert	2017-04-27
\| \| *	Add transparent_abstract tactic	Jason Gross	2017-04-25
* \| \|	[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] Remove `Loc.internal_ghost`	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 tactics.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
\| \|/ \|/\|
\| *	Removing various tactic compatibility layers in core tactics.	Pierre-Marie Pédrot	2017-04-24
\|/
*	Remove VernacError	Gaetan Gilbert	2017-04-21
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\ \
\| * \|	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
* \| \|	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\| \|\ \
* \| \| \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \|/ / \|/\| \|
* \| \|	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
\| \| \|\ \ \| \|_\|/ / \|/\| \| \|