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
*	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
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Classops 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
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Evardefine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Find_subterm 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
\|\
\| *	Removing dead code.	Hugo Herbelin	2016-10-29
\| *	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\| \|\
\| * \	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.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\ \ \
* \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \| \|
\| \| * \| \|	Fix a bug in error printing of unif constraints	Matthieu Sozeau	2016-10-22
\| * \| \| \|	[search] Don't build intermediate lists in search.	Emilio Jesus Gallego Arias	2016-10-20
\| \| \| \| *	[pp] Add tagging function to all low-level printing calls.	Emilio Jesus Gallego Arias	2016-10-18
\| \| \|_\|/ \| \|/\| \|
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-18
\|\\| \| \|
\| * \| \|	[toplevel] Remove undocumented "just_parsing" flag.	Emilio Jesus Gallego Arias	2016-10-17
\| * \| \|	[toplevel] Remove duplicate beautify flags.	Emilio Jesus Gallego Arias	2016-10-17
\| * \| \|	Vernac.ml: inlining read_vernac_file within load_vernac.	Hugo Herbelin	2016-10-17
\| * \| \|	Grouping checks about commands together.	Hugo Herbelin	2016-10-17
\| * \| \|	Vernac.ml: parenthesizing a side-effect.	Hugo Herbelin	2016-10-17
\| * \| \|	Factorizing two instances of load_vernac.	Hugo Herbelin	2016-10-17
\| * \| \|	Passing chan_beautify functionally rather than by side-effect.	Hugo Herbelin	2016-10-17
\| * \| \|	Applying Emilio's suggestion to simplify type of eval_expr.	Hugo Herbelin	2016-10-17
\| * \| \|	More on making the lexer more functional (continuing b8ae2de5 and	Hugo Herbelin	2016-10-17
\| * \| \|	Removing export of location_table outside of cLexer.	Hugo Herbelin	2016-10-17
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\| \| \|
\| * \| \|	Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".	Pierre-Marie Pédrot	2016-10-16
\| \| \|/ \| \|/\|
\| * \|	Merge PR #224 into v8.6	Pierre-Marie Pédrot	2016-10-12
\| \|\ \
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \| \|
\| * \| \|	Fixing #5133 (error reporting delayed).	Hugo Herbelin	2016-10-10
\| \| \| *	A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).	Hugo Herbelin	2016-10-09
\| * \| \|	Moving Pp.comments to CLexer so that Pp is purer (no more side-effect	Hugo Herbelin	2016-10-09