coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
*	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers related to printing.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Eliminating parts of the right-hand side compatibility layer	Pierre-Marie Pédrot	2017-02-14
*	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping 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
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\
\| *	Merge remote-tracking branch 'github/pr/337' into v8.6	Maxime Dénès	2016-10-28
\| \|\
\| \| *	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \|
\| * \|	[search] Don't build intermediate lists in search.	Emilio Jesus Gallego Arias	2016-10-20
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-18
\|\\| \|
\| * \|	More on making the lexer more functional (continuing b8ae2de5 and	Hugo Herbelin	2016-10-17
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\|
\| *	Fix bug #5125: Bad error message when attempting to use where with Class.	Pierre-Marie Pédrot	2016-10-07
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\ \
\| \| *	Add command 'Set foo Append "bar"' for appending to an option (bug #5109).	Guillaume Melquiond	2016-10-01
\| \|/
\| *	In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112)	Enrico Tassi	2016-09-30
\| *	Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl	Enrico Tassi	2016-09-30
\| *	Arguments: cleanup + detect discrepancy rename/implicit (#3753)	Enrico Tassi	2016-09-29
\| *	Merge branch 'bug4723' into v8.6	Matthieu Sozeau	2016-09-29
\| \|\
\| \| *	Cleanup API, making inference_hook optional	Matthieu Sozeau	2016-09-29
\| * \|	Argument : assert does fail if no arg is given (fix #4864)	Enrico Tassi	2016-09-29
\| \| *	Fix bug #4723 and FIXME in API for solve_by_tac	Matthieu Sozeau	2016-09-28
\| \|/
* \|	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
\|\ \
* \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Make it explicit when paths are added to the ML search paths.	Guillaume Melquiond	2016-09-09
\| \| *	Making Proof_global terminator generic in external tactics.	Pierre-Marie Pédrot	2016-09-08
\| \| *	Unplugging Tacexpr in several interface files.	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-02
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
\| * \|	Support qualified identifiers in Show Match (bug #5050).	Guillaume Melquiond	2016-08-27
* \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\\| \|
\| * \|	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24