coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-11	Tentatively more informative report of failure when inferring	Hugo Herbelin
2014-12-08	Fixing wrong evar_map in return clause inference, revealed by 48509b611.	Hugo Herbelin
2014-12-07	Improved tracking of the origin of evars.	Hugo Herbelin
2014-10-22	Fixing an evar leak in pattern-matching compilation (#3758).	Hugo Herbelin
2014-10-17	When facing problem ?id = ?id' in resolution of return predicate,	Hugo Herbelin
2014-10-15	Make use of unfolded primitive projections when elaborating match on a	Matthieu Sozeau
2014-10-13	Added support for several impossible cases in compilation of "match".	Hugo Herbelin
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-10-05	A few improvements on pattern-matching compilation.	Hugo Herbelin
2014-10-04	A few Global.env removed.	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-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-12	An old typo which was preventing example #3537 to work the same as it	Hugo Herbelin
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-06	Fix bug #3584, elaborating pattern-matching on primitive records to the	Matthieu Sozeau
2014-09-04	Typing.sort_of does not leak evarmaps anymore.	Pierre-Marie Pédrot
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-06-26	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau
2014-06-24	Fix program cases and inversion tactic to correctly record universe constraints.	Matthieu Sozeau
2014-06-20	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau
2014-06-04	Collecting in Namegen those conventional default names that are used in diffe...	Hugo Herbelin
2014-05-06	Refresh some universes in cases.ml as they might appear in the term.	Matthieu Sozeau
2014-05-06	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-02-12	TC: honor the use_typeclasses flag in pretyping	Enrico Tassi
2013-12-06	Fix test-suite/success/evars.v.	Arnaud Spiwack
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-02	Fix compilation of pattern matching wrt variables: alias.	aspiwack
2013-11-02	Fix the compilation of pattern matching wrt to variables.	aspiwack
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-05-11	Fixing a source of evars leak, revealed by contrib QuicksortComplexity	herbelin
2013-05-09	Uniformization: isevars -> evdref/sigma/evd	herbelin
2013-04-30	Fix wrong computation of dependency signature in cases raising an uncaught ex...	msozeau
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-02-18	Removing Exc_located and using the new exception enrichement	ppedrot
2013-02-18	use List.rev_map whenever possible	letouzey
2013-02-10	Splitted Evarutil in two files	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-19	Array.create is deprecated	pboutill