coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
*	[native_compute] Remove useless conversion to list in reification.	Maxime Dénès	2018-02-05
*	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
*	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert	2017-09-29
*	use OCaml 4.03-compatible Filename functions	Paul Steckler	2017-08-22
*	use OCaml temp_file, instead of our own version	Paul Steckler	2017-08-18
*	move filename search to start_profiler	Paul Steckler	2017-08-18
*	Add native compute profiling, BZ#5170	Paul Steckler	2017-08-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Don't double up on periods in anomalies	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
*	Inv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Nativenorm API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	CLEANUP: using \|> operator more consistently	Matej Kosik	2016-08-30
*	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fix bug in native compiler with universe polymorphism.	Maxime Dénès	2015-10-28
*	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
*	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
*	Make normalization of primitive projections in native_compute the same as wit...	Maxime Dénès	2015-06-08
*	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix for #3154: use CUnix.sys_command to call native compiler.	Maxime Dénès	2014-12-16
*	Fix #3824. de Bruijn error in normalization of fixpoints.	Maxime Dénès	2014-11-23
*	Fix missing lift in VM and native compiler (second part of #2729).	Maxime Dénès	2014-10-22
*	Porting Hugo's fix 98f3abb83a to native compiler.	Maxime Dénès	2014-10-21
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Readback for int31 values from native compiler.	Maxime Dénès	2014-04-09
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Native compiler: timing info for reification in debug mode.	mdenes	2013-03-25
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05