coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Bump year in headers.	Maxime Dénès	2017-06-01
\|
*	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\|
*	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| \| \| \|	This saves a quadratic allocation by replacing arrays with maps.
*	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| \| \| \| \|	In addition to sharing, we also delay the computation of the environment in a by-need fashion.
*	Use sets instead of lists for names to avoid in evar generation.	Pierre-Marie Pédrot	2016-08-04
\|
*	Simplifying code in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| \| \| \| \| \| \|	We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences.
*	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot	2016-08-04
\|
*	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\|
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20