coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	set_solve_evars doesn't use an evar_map ref	Gaëtan Gilbert	2018-05-11
*	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
*	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Renamings to avoid confusion deprecating old names	Matthieu Sozeau	2016-10-22
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Documenting check_record + changing a possibly undefined int into int option.	Hugo Herbelin	2014-12-15
*	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau	2014-12-12
*	Setup hook to change the unification algorithm used by evarconv,	Matthieu Sozeau	2014-12-09
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	2014-09-26
*	- Fix bug #3368, due to wrong use of the Cst_stack for projections.	Matthieu Sozeau	2014-06-11
*	Cst_stack before stack (abstraction leak in whd_gen)	Pierre Boutillier	2014-05-26
*	- Add back some compatibility functions to avoid rewriting plugins.	Matthieu Sozeau	2014-05-06
*	- Fixes for canonical structure resolution (check that the initial term indee...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	consider_remaining_unif_problems respects Conv_oracle	Pierre Boutillier	2014-03-16
*	Evarconv unification respects Conv_oracle	Pierre Boutillier	2014-03-10
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Reductionops.Stack.strip* are ready to deal with Shift	Pierre Boutillier	2014-02-24
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	comments in mli	pboutill	2013-05-30
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	A few comments in evarconv.mli.	herbelin	2013-05-09
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Refined second_order_matching so that a constraint on which	herbelin	2011-11-08
*	Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed	herbelin	2011-10-11
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Reverted commit r13893 about propagation of more informative	herbelin	2011-03-07
*	Added propagation of evars unification failure reasons for better	herbelin	2011-03-07
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29