coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\|
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| *	Hints/Univs: fix bug #4628 anomalies	Matthieu Sozeau	2016-05-23
* \|	Relying on generic arguments to represent Extern hints.	Pierre-Marie Pédrot	2016-03-20
* \|	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot	2016-03-20
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \|	Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.	Pierre-Marie Pédrot	2015-12-28
\|/
*	Fix bug #4433, removing hack on evars appearing in a pattern from a	Matthieu Sozeau	2015-11-19
*	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau	2015-11-04
*	Fixing a loop in checking hints with holes.	Hugo Herbelin	2015-10-24
*	Merge hint lists instead of appending them. (Fix bug #3199)	Guillaume Melquiond	2015-10-16
*	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
*	Fix CFGV contrib: handling of global hints introducing global universes.	Matthieu Sozeau	2015-10-09
*	Fix bug #4354: interpret hints in the right env and sigma.	Matthieu Sozeau	2015-10-06
*	Univs: fix evar_map handling in Hint processing.	Matthieu Sozeau	2015-10-02
*	Univs: fix many evar_map initializations and leaks.	Matthieu Sozeau	2015-10-02
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Adding an option Loose Hint Behavior to handle hints loaded but not imported.	Pierre-Marie Pédrot	2015-05-12
*	Adding unique identifiers to hints.	Pierre-Marie Pédrot	2015-05-12
*	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot	2015-05-11
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Ensuring purity of datastructures in the API.	Pierre-Marie Pédrot	2015-04-16
*	Cleaning up the implementation of search entries in Hints.	Pierre-Marie Pédrot	2015-04-14
*	Opaque implementation of auto tactics.	Pierre-Marie Pédrot	2015-04-14
*	More documented representation of hint objects.	Pierre-Marie Pédrot	2015-04-13
*	Fix bug #3590, keeping evars that are not turned into named metas by	Matthieu Sozeau	2015-03-03
*	Update headers.	Maxime Dénès	2015-01-12
*	Removing the last Evd.diff from Hints.	Pierre-Marie Pédrot	2014-10-27
*	Forgotten hints.ml{,i} files in 38b34dfffcc.	Hugo Herbelin	2014-10-08