coq - The formal proof system

Age	Commit message (Expand)	Author
2019-01-09	Stop [Print] from saying [is (not) universe polymorphic].	Gaëtan Gilbert
2018-12-17	Stop printing Monomorphic/Polymorphic in Print.	Gaëtan Gilbert
2018-11-02	Remove is_universe_polymorphism from printing	Gaëtan Gilbert
2018-03-09	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès
2018-03-08	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias
2018-02-22	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin
2017-05-30	Support for using type information to infer more precise evar sources.	Hugo Herbelin
2017-04-04	Merge branch 'trunk' into pr379	Maxime Dénès
2017-03-24	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin
2017-02-14	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot
2016-02-13	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
2015-11-08	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin
2015-06-24	Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.	Maxime Dénès
2015-03-09	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond
2014-10-21	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin
2014-09-18	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier
2014-05-08	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot
2013-10-08	Fixing 2 output test-suites.	ppedrot
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-02-25	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill
2011-12-04	A small test for type inference (used to be a regression at some time).	herbelin