coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using "__" rather than this unelegant arbitrary "A" for the name of variables...	Hugo Herbelin	2015-10-18
*	Using appropriate lambda decomposition function counting let-ins when	Hugo Herbelin	2015-10-18
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Do not compress match constructs when the inner match contains no branch. (Fi...	Guillaume Melquiond	2015-09-18
*	Continuing experimentation on what part of the instance of an evar	Hugo Herbelin	2015-02-21
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Reactivating option "Set Printing Existential Instances" for asking printing ...	Hugo Herbelin	2014-12-04
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	New experimental heuristic printing strategy for evar instances: We	Hugo Herbelin	2014-10-17
*	Re-displaying evar instances in debugger.	Hugo Herbelin	2014-10-17
*	Add an option to not print primitive projection parameters, which can	Matthieu Sozeau	2014-10-15
*	Make constrMatching and detyping more robust with respect to	Matthieu Sozeau	2014-10-10
*	Avoid a warning with Meta's names in debugger.	Hugo Herbelin	2014-10-07
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Fix incorrect assert false in detyping.	Matthieu Sozeau	2014-09-25
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin	2014-09-13
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Fixing the essence of naming bug #3204: use same strategy for naming	Hugo Herbelin	2014-08-25
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Compute the trace of a universe inconsistency only when explicitly required	Pierre-Marie Pédrot	2014-06-10
*	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	Goptions do not rely anymore on generic equality.	Pierre-Marie Pédrot	2014-03-03
*	Fixing bad comparison in Detyping.	Pierre-Marie Pédrot	2014-03-01
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	2013-11-25
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Improving formatting of output of "Test table".	herbelin	2013-01-27
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of name	ppedrot	2012-12-18
*	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin	2012-12-17
*	Modulification of identifier	ppedrot	2012-12-14