coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-16	Documenting the removal of coercions between sig, sigT, sig2,	Hugo Herbelin
2015-01-16	Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"	Matthieu Sozeau
2015-01-15	vm_printers: fix compilation	Enrico Tassi
2015-01-15	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau
2015-01-15	Minor fixes to the refman credits to be continued.	Matthieu Sozeau
2015-01-15	Move explanations about primitive projections to the manual.	Matthieu Sozeau
2015-01-15	Add a (by default deactivated) option to force typeclass resolution to	Matthieu Sozeau
2015-01-15	Expand Credits for 8.5 and doc on universes	Matthieu Sozeau
2015-01-15	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau
2015-01-15	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau
2015-01-15	Update header of CHANGES.	Maxime Dénès
2015-01-15	Remove left-over dead code in previous commit.	Maxime Dénès
2015-01-15	Make -print-mod-uid accept a list of files.	Maxime Dénès
2015-01-15	Mention CHANGES file in COMPATIBILITY.	Maxime Dénès
2015-01-15	Mention guard condition in CHANGES.	Maxime Dénès
2015-01-15	Make installation of native files more robust.	Maxime Dénès
2015-01-15	coq_makefile installs native files	Pierre Boutillier
2015-01-15	Always build (even when -coqide no) and install idetoploop	Pierre Boutillier
2015-01-15	Hugo put me in credits, but I was already there :)	Maxime Dénès
2015-01-15	Tentatively updating credits while remaining brief.	Hugo Herbelin
2015-01-14	Makefile: install ide/*lang	Enrico Tassi
2015-01-14	coq_makefile: chmod 755 on toplopp cmxs	Enrico Tassi
2015-01-14	CoqIDE: a Make file to build coqidetop toploop	Enrico Tassi
2015-01-14	Reference manual: I had previously omitted the syntax entry for [> t1\|…\|tn].	Arnaud Spiwack
2015-01-14	Reference manual: document tryif/then/else.	Arnaud Spiwack
2015-01-14	Reference manual: document multimatch.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve documentation for Ltac's match.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve the documentation of lazymatch.	Arnaud Spiwack
2015-01-14	Reference manual: document gfail.	Arnaud Spiwack
2015-01-14	CHANGES: my recent updates to Ltac.	Arnaud Spiwack
2015-01-13	Bump version and magic numbers in configure.	Maxime Dénès
2015-01-13	Made -print-mod-uid more silent and robust.	Maxime Dénès
2015-01-13	Refresh some copyright headers.	Maxime Dénès
2015-01-13	Native compiler: if debug flag not present, remove .native files.	Maxime Dénès
2015-01-13	More documentation of the Local Definitions and Axioms.	Pierre-Marie Pédrot
2015-01-13	More in CHANGES about local definitions	Pierre-Marie Pédrot
2015-01-13	TCs: Properly handle Hint Extern with conclusions of the form _ -> _	Matthieu Sozeau
2015-01-13	Fix test-suite file, we were testing that no anomaly was raised	Matthieu Sozeau
2015-01-13	Update hash of cic.mli in checker/values.ml,	Matthieu Sozeau
2015-01-13	Fix bug when discharging universe constraints coming from variables	Matthieu Sozeau
2015-01-13	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau
2015-01-12	typo in coqide compilation rules after -thread requirement	Pierre Boutillier
2015-01-12	Derive -> derive occurences	Pierre Boutillier
2015-01-12	Coq_makefile erases native compiler files	Pierre Boutillier
2015-01-12	fixup to vi -> vio renaming	Enrico Tassi
2015-01-12	Whodidwhat-8.5: a global pass	Arnaud Spiwack
2015-01-12	whodidwhat-8.5: typo.	Arnaud Spiwack
2015-01-12	Add -no-native-compiler flag to list dumped by --help.	Maxime Dénès
2015-01-12	Add myself to credits.	Maxime Dénès
2015-01-12	Update credits.	Guillaume Melquiond