coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	More consistent writing of de Bruijn.	Théo Zimmermann	2017-05-01
*	Fix for bug 5507. Mispelt de Bruijn.	Théo Zimmermann	2017-05-01
*	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
\|/ /
* \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
* \|	Moving three related small half-general half-ad-hoc utility functions	Hugo Herbelin	2015-12-05
\|/
*	Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,	Hugo Herbelin	2015-10-18
*	Update headers.	Maxime Dénès	2015-01-12
*	Revert "Term: include a function to print terms"	Enrico Tassi	2014-12-27
*	Term: include a function to print terms	Enrico Tassi	2014-12-26
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Simplify evarconv thanks to new delta status of projections,	Matthieu Sozeau	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Do not generate useless argument arrays in whd_* functions.	ppedrot	2013-10-29
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Removing two Pervasives.compare from Term.	ppedrot	2013-04-03
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05
*	avoid (Int.equal (cmp ...) 0) when a boolean equality exists	letouzey	2013-02-19
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	* Kernel/Terms:	regisgia	2013-01-06
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Fixing a comment.	herbelin	2012-12-04
*	Removed some FIXME related to equality on universes.	ppedrot	2012-11-26
*	Monomorphization (kernel)	ppedrot	2012-11-22
*	More monomorphizations	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02