coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \|	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
\|/ /
* \|	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
\| *	Goal selectors now use the keyword [only].	Cyprien Mangin	2016-06-30
\|/
*	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