coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-01-20	Update copyright headers.	Maxime Dénès

2015-11-04	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau
	inconsistent).
2015-10-14	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot

2015-10-09	Refine fix for handling of the universe contexts of hints, depending on	Matthieu Sozeau
	their polymorphic status _and_ locality.
2015-10-09	Fix CFGV contrib: handling of global hints introducing global universes.	Matthieu Sozeau
	It was wrong, the context was readded needlessly to the local evar_map context.
2015-10-06	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau

2015-05-11	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot

2015-04-14	Opaque implementation of auto tactics.	Pierre-Marie Pédrot
	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.
2015-04-12	Making the hint entry type opaque.	Pierre-Marie Pédrot

2015-04-10	Making the hints for the auto tactics private.	Pierre-Marie Pédrot
	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.
2015-01-12	Update headers.	Maxime Dénès

2014-10-08	Forgotten hints.ml{,i} files in 38b34dfffcc.	Hugo Herbelin