coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-10-21	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau

2016-09-05	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot
	Essentially, we do not reconstruct the named_context_val when the rel_context is empty.
2016-09-02	Fast path in whd_evar.	Pierre-Marie Pédrot
	Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined.
2016-08-06	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot
	This saves a quadratic allocation by replacing arrays with maps.
2016-08-05	Using the extended contexts in pretyping.	Pierre-Marie Pédrot
	In addition to sharing, we also delay the computation of the environment in a by-need fashion.
2016-08-04	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
	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.
2016-08-04	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot

2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-06-24	Optimize the clear tactic.	Pierre-Marie Pédrot
	We do not allocate a closure in the main loop, and do so only when needed.
2016-06-24	Optimize the clear tactic.	Pierre-Marie Pédrot
	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.
2016-06-16	Document new Hint Mode option.	Matthieu Sozeau

2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot

2016-03-20	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot