coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-12-02
*	Fix bug #5232: proper globalization of hints paths	Matthieu Sozeau	2016-11-30
*	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\|\
\| *	Fixes to compile with ocaml 4.01	Matthieu Sozeau	2016-11-07
* \|	Merge commit 'e6edb33' into v8.6	Maxime Dénès	2016-11-07
\|\ \
\| * \|	More explicit name for status of unification constraints.	Maxime Dénès	2016-11-07
\| \| *	Rework search_strategy option handling	Matthieu Sozeau	2016-11-03
\| \| *	Fix handling of only_classes at toplevel	Matthieu Sozeau	2016-11-03
\| \| *	Fix Typeclasses eauto := bfs.	Matthieu Sozeau	2016-11-03
\| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
\| \|/ \|/\|
* \|	Fixing #5164 (regression in locating error in argument of "refine").	Hugo Herbelin	2016-10-29
* \|	Merge branch 'v8.5' into v8.6	Hugo Herbelin	2016-10-22
\| *	Unification constraint handling (#4763, #5149)	Matthieu Sozeau	2016-10-22
\|/
*	Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3	Matthieu Sozeau	2016-10-21
*	Merge branch 'bug5036' into v8.6	Matthieu Sozeau	2016-10-20
\|\
\| *	Fix bug #5036 autorewrite, sections and universes	Matthieu Sozeau	2016-10-20
* \|	Fix bug #5116: [Print Ltac] should be able to print strategies.	Pierre-Marie Pédrot	2016-10-12
* \|	Fix bug #5098: Symmetry broken in HoTT.	Pierre-Marie Pédrot	2016-10-08
* \|	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
\|\
* \|	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