coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
*	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\
\| *	Moving Tacexpr to ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| *	Made Ppanotation Ltac-agnostic.	Pierre-Marie Pédrot	2016-09-15
\| *	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
\| *	Moving Tactic_matching to ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| *	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| *	Moving Ltac printers to ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| *	Generalizing the notion of constr substitution to generic arguments.	Pierre-Marie Pédrot	2016-09-15
\| *	Moving Ltac-specific parsing API to ltac/ folder.	Pierre-Marie Pédrot	2016-09-14
\| *	Moving the tactic-in-term extension from G_constr to G_ltac.	Pierre-Marie Pédrot	2016-09-14
\| *	Allowing to extend the Print Grammar command generically.	Pierre-Marie Pédrot	2016-09-14
* \|	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
\| \| *	Move Ltac-specific components from G_proofs to G_ltac.	Pierre-Marie Pédrot	2016-09-11
\| * \|	Fix bug #3920 for good after 44ada64.	Pierre-Marie Pédrot	2016-09-09
\| \| *	Unplugging Pptactic from Ppvernac.	Pierre-Marie Pédrot	2016-09-08
\| \| *	Making Proof_global terminator generic in external tactics.	Pierre-Marie Pédrot	2016-09-08
\| \| *	Making Hints generic in the use of external tactics.	Pierre-Marie Pédrot	2016-09-08
\| \| *	Making Vernacexpr independent from Tacexpr.	Pierre-Marie Pédrot	2016-09-08
\| \|/ \|/\|
* \|	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
\|/