coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Fixing #5078 (wrong detection of evaluable local hypotheses).	Hugo Herbelin	2016-09-13
\| *	LtacProp: fix reset_profile (fix #5079)	Enrico Tassi	2016-09-13
\| *	Fix newlines in printout of LtacProf	Jason Gross	2016-09-11
\| *	Revert the LtacProf tactic table header	Jason Gross	2016-09-11
\| *	Fix bug #3920 for good after 44ada64.	Pierre-Marie Pédrot	2016-09-09
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Removing useless tactic compatibility layer in Rewrite.	Pierre-Marie Pédrot	2016-09-07
\| * \|	ltacprof: rec-calls are coaleshed	Enrico Tassi	2016-09-07
\| * \|	profile_ltac: rewritten to be purely functional and STM aware	Enrico Tassi	2016-09-05
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\\| \|
\| * \|	Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal	Hugo Herbelin	2016-09-01
\| * \|	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
\| * \|	Fix bug #3920: eapply masks an hypothesis name.	Pierre-Marie Pédrot	2016-08-30
* \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\\| \|
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| * \|	Fix bug #4914: LtacProf printout has too many newlines.	Pierre-Marie Pédrot	2016-08-23
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-21
\|\\| \|
\| * \|	Moving Taccoerce to ltac/ folder.	Pierre-Marie Pédrot	2016-08-19
\| \| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| \| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| \| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\| \|/ \|/\|
\| *	Merge remote-tracking branch 'github/bug4188' into v8.6	Matthieu Sozeau	2016-08-18
\| \|\
\| * \|	Fix bug #4939: LtacProf prints tactic notations weirdly.	Pierre-Marie Pédrot	2016-08-18
\| \| *	Fix setoid_rewrite to raise proper errors	Matthieu Sozeau	2016-08-17
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-17
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\| *	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
* \|	Merge branch 'v8.6' into trunk	Pierre Letouzey	2016-07-26
\|\\|
\| *	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
* \|	Renouncing for uniformity to the few instances of pf_interp_* in Tacinterp.	Hugo Herbelin	2016-07-12
\|/
*	Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...	Maxime Dénès	2016-07-04
*	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
*	rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...	Pierre Letouzey	2016-07-03
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	LtacProf reports structured results (pr/209)	CJ Bell	2016-06-20
*	Do not evar-normalize goals when interpreting some hardwired genargs.	Pierre-Marie Pédrot	2016-06-20
*	Backporting c064fb933 from 8.5 (another regression with Ltac trace report).	Hugo Herbelin	2016-06-18
*	Adding an "as" clause to specialize.	Hugo Herbelin	2016-06-18
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Exporting a generic argument induction_arg. As a consequence,	Hugo Herbelin	2016-06-18
*	Adding eintros to respect the e- prefix policy.	Hugo Herbelin	2016-06-18
*	par: like all: but in parallel	Enrico Tassi	2016-06-17
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16