coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
\| \| \| \|	inconsistent).
*	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot	2015-10-14
\|
*	Refine fix for handling of the universe contexts of hints, depending on	Matthieu Sozeau	2015-10-09
\| \| \| \|	their polymorphic status _and_ locality.
*	Fix CFGV contrib: handling of global hints introducing global universes.	Matthieu Sozeau	2015-10-09
\| \| \| \|	It was wrong, the context was readded needlessly to the local evar_map context.
*	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
\|
*	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
\|
*	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
\| \| \| \| \| \|	We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility.
*	Making the hint entry type opaque.	Pierre-Marie Pédrot	2015-04-12
\|
*	Making the hints for the auto tactics private.	Pierre-Marie Pédrot	2015-04-10
\| \| \| \| \| \|	They are all generated by the Hints module, and making them purely opaque is not worthwhile because we project them a lot. This ensures that they all get generated following a uniform process.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Forgotten hints.ml{,i} files in 38b34dfffcc.	Hugo Herbelin	2014-10-08