coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-17	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-13	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
2014-12-04	Reactivating option "Set Printing Existential Instances" for asking printing ...	Hugo Herbelin
2014-11-19	Printing function for [uconstr].	Arnaud Spiwack
2014-10-20	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin
2014-10-17	New experimental heuristic printing strategy for evar instances: We	Hugo Herbelin
2014-10-17	Re-displaying evar instances in debugger.	Hugo Herbelin
2014-10-15	Add an option to not print primitive projection parameters, which can	Matthieu Sozeau
2014-10-10	Make constrMatching and detyping more robust with respect to	Matthieu Sozeau
2014-10-07	Avoid a warning with Meta's names in debugger.	Hugo Herbelin
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
2014-09-25	Fix incorrect assert false in detyping.	Matthieu Sozeau
2014-09-18	Fix debug printing with primitive projections.	Matthieu Sozeau
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-13	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin
2014-09-12	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-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-08-25	Fixing the essence of naming bug #3204: use same strategy for naming	Hugo Herbelin
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-07-01	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau
2014-06-10	Compute the trace of a universe inconsistency only when explicitly required	Pierre-Marie Pédrot
2014-06-04	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-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin
2014-03-03	Goptions do not rely anymore on generic equality.	Pierre-Marie Pédrot
2014-03-01	Fixing bad comparison in Detyping.	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-25	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin
2013-10-23	cList.index is now cList.index_f, same for index0	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2013-01-27	Improving formatting of output of "Test table".	herbelin
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
2012-12-18	Modulification of name	ppedrot
2012-12-17	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin
2012-12-14	Modulification of identifier	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia