coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
\|
*	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
\| \| \| \| \| \| \|	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
*	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot	2017-06-16
\|
*	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").	Maxime Dénès	2017-06-14
\|\ \
\| \| *	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
* \| \|	Dualize the unsafe flag of refine into typecheck and make it mandatory.	Pierre-Marie Pédrot	2017-06-13
\| \|/ \|/\|
* \|	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\ \
* \| \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| \| \|
\| * \|	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\|/ /
\| *	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\|/ \| \| \| \| \| \| \| \|	Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
*	Put "ssreflect" behind "API".	Matej Košík	2017-06-07
\|
*	Merge the ssr plugin.	Maxime Dénès	2017-06-06