coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
\| *	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin	2017-03-24
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\
\| *	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
* \|	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin	2015-11-08
\|/
*	Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.	Maxime Dénès	2015-06-24
*	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond	2015-03-09
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
*	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot	2014-05-08
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	A small test for type inference (used to be a regression at some time).	herbelin	2011-12-04