coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Hipattern API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Clenv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Typeclasses API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Tacred API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Constr_matching API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Patternops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	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
\| *	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