coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
*	Unify pre_env and env	Maxime Dénès	2018-05-28
*	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] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
*	Fast environment lookup for rels.	Pierre-Marie Pédrot	2017-12-29
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in 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
*	Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.	Hugo Herbelin	2017-08-12
*	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
*	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
*	Removing a redundant universe instance information in native compute.	Pierre-Marie Pédrot	2017-07-10
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	Remove dead code in native compiler.	Maxime Dénès	2017-05-02
*	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
\| *	Fix bug #5435: [Eval native_compute in] raises anomaly.	Maxime Dénès	2017-04-04
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-09
\| \|\ \
\| \| \| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\| \| * \|	Restore native compiler optimizations after they were broken by 9e2ee58.	Maxime Dénès	2016-09-09
\| \| \| *	Packing the named_context_val in a proper record and marking it private.	Pierre-Marie Pédrot	2016-09-09
\| \| \|/ \| \|/\|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\\| \|
\| * \|	More efficient data structure to check if a native file is loaded.	Maxime Dénès	2016-09-01
* \| \|	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
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| *	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
* \|	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
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Fixing some English misspelling.	Hugo Herbelin	2015-07-29
*	Native compiler: refactor code handling pre-computed values.	Maxime Dénès	2015-07-10
*	Fix native compilation of primitive projections. Closes #4210.	Maxime Dénès	2015-06-08
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Cleaner interfaces for linking locations of native compiler.	Maxime Dénès	2014-11-12
*	No hash consing across calls to the native compiler.	Maxime Dénès	2014-10-24
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20