coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\
* \	Merge branch "LtacProf for trunk" (PR #165).	Pierre-Marie Pédrot	2016-06-14
\|\ \
\| * \|	Commenting out debugging code.	Pierre-Marie Pédrot	2016-06-14
\| * \|	Correct use of printing primitives.	Pierre-Marie Pédrot	2016-06-14
\| * \|	Better coding style (semantics).	Pierre-Marie Pédrot	2016-06-14
\| * \|	Better coding style (syntax).	Pierre-Marie Pédrot	2016-06-14
\| * \|	Adding Coq headers.	Pierre-Marie Pédrot	2016-06-14
\| * \|	Moving back Ltac profiling to the Ltac folder.	Pierre-Marie Pédrot	2016-06-14
\| * \|	Revert "Strip some trailing spaces"	Pierre-Marie Pédrot	2016-06-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
* \| \|	About printing of traces of failures while calling ltac code.	Hugo Herbelin	2016-06-06
\| \| *	STM: proof block detection for par:	Enrico Tassi	2016-06-06
\| \| *	STM: proof block detection/error resilience API	Enrico Tassi	2016-06-06
\| \|/ \|/\|
\| *	Make Ltac Profiling an setting	Jason Gross	2016-06-05
\| *	Synchronize the profiler state with the document	Jason Gross	2016-06-05
\| *	LtacProf for Coq trunk	Jason Gross	2016-06-05
\| *	Strip some trailing spaces	Jason Gross	2016-06-05
\|/
*	Adding the Print Ltac Signature command.	Pierre-Marie Pédrot	2016-06-05
*	Removing "rename" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "exact" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Removing "double induction" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
*	Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.	Hugo Herbelin	2016-06-02
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "move" tactic in the monad.	Pierre-Marie Pédrot	2016-05-17
*	Put the "change" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "specialize_eq" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "generalize dependent" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "cofix" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "*_cast_no_check" tactics in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Put the "exact" family of 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
*	Generate more user-readable tactic notation kernel names.	Pierre-Marie Pédrot	2016-05-16
*	Making the grammar command extend API purely functional.	Pierre-Marie Pédrot	2016-05-11
*	Moving the constr empty entry registering to the state-based API.	Pierre-Marie Pédrot	2016-05-11
*	Turning the grammar extend command API into a state-passing one.	Pierre-Marie Pédrot	2016-05-11
*	Moving the grammar summary to Pcoq.	Pierre-Marie Pédrot	2016-05-11
*	AlistNsep token now accepts an arbitrary separator.	Pierre-Marie Pédrot	2016-05-10
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
*	Pass user symbol to tactic notation printers.	Pierre-Marie Pédrot	2016-05-08
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
*	Removing useless generic arguments.	Pierre-Marie Pédrot	2016-05-04
*	Interpretation function can return any untyped value.	Pierre-Marie Pédrot	2016-05-04
*	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
*	Removing the Value.of_* API for parameterized types.	Pierre-Marie Pédrot	2016-05-04