coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\
\| *	Fix bug #5116: [Print Ltac] should be able to print strategies.	Pierre-Marie Pédrot	2016-10-12
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\|
\| *	Fix bug #5098: Symmetry broken in HoTT.	Pierre-Marie Pédrot	2016-10-08
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	LtacProf cutoff is for total percent, not time	Jason Gross	2016-09-29
\| *	Merge branch 'bug5036' into v8.6	Matthieu Sozeau	2016-09-29
\| \|\
\| \| *	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-09-29
\| * \|	-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)	Enrico Tassi	2016-09-29
\| \|/
\| *	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-27
\|\\| \|
\| * \|	LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)	Enrico Tassi	2016-09-27
\| * \|	Fix bug #5093: typeclasses eauto depth arg does not accept a var.	Pierre-Marie Pédrot	2016-09-26
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\| \|
* \| \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \| \|	Merge remote-tracking branch 'github/pr/283' into trunk	Maxime Dénès	2016-09-22
\|\ \ \
* \| \| \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| * \| \|	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
\| \| * \|	Continuing fix to #5078, taking also into account intropatterns.	Hugo Herbelin	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