coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
*	Typing: define functional alternatives to e_* functions	Gaëtan Gilbert	2018-05-14
*	Deprecate Evarconv.e_conv,e_cumul	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
*	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
*	[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
*	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
*	Clenv 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
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Fixing #5077 (failure on typing a fixpoint with evars in its type).	Hugo Herbelin	2016-09-10
* \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Proofview refiner is now type-safe by default.	Pierre-Marie Pédrot	2014-09-04
*	Typing.sort_of does not leak evarmaps anymore.	Pierre-Marie Pédrot	2014-09-04
*	Fix bug #3559, ensuring a canonical order of universe level quantifications when	Matthieu Sozeau	2014-09-04
*	Refresh universes for Ltac's type_of, as the term can be used anywhere,	Matthieu Sozeau	2014-05-09
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Updating headers.	herbelin	2012-08-08
*	More unification in type_of and addition of e_type_of to get the new	herbelin	2011-10-24
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	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
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Promote evar_defs to evar_map (in Evd)	glondu	2009-11-11
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
*	entetes	filliatr	2001-03-15
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin	2000-10-18
*	mise au point Declare et avancee dans Astterm	filliatr	1999-12-01
*	- environment -> safe_environment	filliatr	1999-12-01
*	- Typing -> Safe_typing	filliatr	1999-12-01