coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\
* \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
\| *	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\|/
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing the old refine tactic from the Tactics module.	Pierre-Marie Pédrot	2016-05-17
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "fix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "clear" tactic into the monad.	Pierre-Marie Pédrot	2016-05-16
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-04
\|\
\| *	Remove extraneous space in coqtop/pg output (bug #4675).	Guillaume Melquiond	2016-05-03
* \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
* \|	Adding a universe argument to Pcoq.create_generic_entry.	Pierre-Marie Pédrot	2016-03-17
* \|	Removing the registering of default values for generic arguments.	Pierre-Marie Pédrot	2016-03-17
* \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \|	The tactic generic argument now returns a value rather than a glob_expr.	Pierre-Marie Pédrot	2016-02-22
* \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \
* \| \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Constraining refine to monotonic functions.	Pierre-Marie Pédrot	2015-10-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Removing uselessly duplicated function in Evd.	Pierre-Marie Pédrot	2015-09-27
\|/
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Declarative mode: remaining goals are "given up" when closing blocks.	Arnaud Spiwack	2015-04-22
*	Declarative mode: fix proof modes.	Arnaud Spiwack	2015-03-31
*	Declarative mode: fix vernac classification.	Arnaud Spiwack	2015-03-31
*	Declarative mode: plug the specialised printers back.	Arnaud Spiwack	2015-03-31
*	Declarative mode: make it so that unfocussing can only be done for closed sub...	Arnaud Spiwack	2015-03-13
*	Declarative mode: remove dead code.	Arnaud Spiwack	2015-03-13
*	Declarative mode: remove a superfluous [set_proof_mode].	Arnaud Spiwack	2015-03-13
*	Declarative mode: fix the focus behaviour.	Arnaud Spiwack	2015-03-13
*	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-13
*	Fix double print in decl_mode.	Enrico Tassi	2015-03-11
*	Removing the unused field ltacrecvars of tactic internalization.	Pierre-Marie Pédrot	2015-02-27
*	Update headers.	Maxime Dénès	2015-01-12
*	Writing rename_hyps in the new monad.	Pierre-Marie Pédrot	2014-11-03
*	Remove the deprecated open-constr based refine.	Arnaud Spiwack	2014-10-22
*	A version of convert_concl and convert_hyp in new proof engine.	Hugo Herbelin	2014-10-09
*	decl_mode: stay in declarative mode	Enrico Tassi	2014-10-06
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-05
*	Revert the two previous commits. I was testing in the wrong branch.	Pierre-Marie Pédrot	2014-09-04
*	Removing the old implementation of clear_body.	Pierre-Marie Pédrot	2014-09-04