coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \| \| \| \|	There don't really bring anything, we also correct some minor nits with the printing function.
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Added support for a side effect on constants in reduction functions.	Thomas Sibut-Pinote	2017-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
*	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
	For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a