coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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.
*	Unification API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Typing API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\|
\| *	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
\| \| \| \| \| \| \| \|	goal is under focus and which support returning a relevant output.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\| \|
* \|	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.
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Moving Refine to its proper module.	Pierre-Marie Pédrot	2016-03-20