coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\
* \|	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
* \|	Continuing fix to #5078, taking also into account intropatterns.	Hugo Herbelin	2016-09-15
* \|	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
* \|	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
* \|	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
* \|	Fix bug #4914: LtacProf printout has too many newlines.	Pierre-Marie Pédrot	2016-08-23
* \|	Moving Taccoerce to ltac/ folder.	Pierre-Marie Pédrot	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.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
* \|	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
* \|	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
*	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
*	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
*	Typo in comment.	Hugo Herbelin	2016-06-16
*	Fixing space in an error message.	Hugo Herbelin	2016-06-16
*	Fixing printing of Register retroknowledge.	Hugo Herbelin	2016-06-16