coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|\
\| *	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-12-02
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\ \
\| \| *	Fix bug #5232: proper globalization of hints paths	Matthieu Sozeau	2016-11-30
\| \|/
* \|	Fix locality of "Hint Resolve <->" (bug #5189).	Guillaume Melquiond	2016-11-22
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	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
\| \| \|/ \| \|/\|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\| \|
\| * \|	Fixing #5164 (regression in locating error in argument of "refine").	Hugo Herbelin	2016-10-29
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \|
\| * \|	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
* \| \|	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