coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...	Maxime Dénès	2017-12-14
\|\ \
* \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
* \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|/ \|/\|
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
* \|	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\ \
\| * \|	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
* \| \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\|/ /
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
\| *	ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)	Enrico Tassi	2017-11-09
* \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\|/
*	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\
* \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| *	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\|/
*	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot	2017-10-03
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	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
*	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
* \| \|	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
\|/
*	Put "ssreflect" behind "API".	Matej Košík	2017-06-07
*	Merge the ssr plugin.	Maxime Dénès	2017-06-06