coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing some return type compatibility layers in Termops.	Pierre-Marie Pédrot	2017-02-14
\|
*	Proofview.Goal primitive now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
\|
*	Rewrite API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Leminv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Refine API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| \| \| \| \| \| \| \|	This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
*	Pretyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evarconv API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Evarsolve API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	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