coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\
\| *	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-10-21
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\\|
\| *	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot	2016-09-05
\| \| \| \| \| \| \| \| \| \|	Essentially, we do not reconstruct the named_context_val when the rel_context is empty.
\| *	Fast path in whd_evar.	Pierre-Marie Pédrot	2016-09-02
\| \| \| \| \| \| \| \| \| \|	Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined.
* \|	Removing calls of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-26
\| \|
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-26
\| \|
* \|	CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵	Matej Kosik	2016-08-25
\| \| \| \| \| \| \| \|	"Context.{Rel,Named}.fold_constr"
* \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\|/ \| \| \| \| \| \| \| \| \| \|	mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
*	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
\|
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| \| \| \|	We do not allocate a closure in the main loop, and do so only when needed.
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| \| \| \| \|	We do not check for presence of a variable in a global definition when we know that this variable was not present in the section.
*	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
\|
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20