coq - The formal proof system

Age	Commit message (Expand)	Author
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-09-24	Adding evar printing to debugger.	ppedrot
2013-09-24	Fixing ocamldebug compilation by adding thread linking.	ppedrot
2013-09-20	Fix name clash in "failure/inductive.v".	xclerc
2013-09-20	Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.	xclerc
2013-09-20	Merge "inductive?.v" tests into a single "inductive.v" test.	xclerc
2013-09-20	Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.	xclerc
2013-09-20	Get rid of "shouldfail" subdirectory by moving tests to parent directory.	xclerc
2013-09-20	Wrong bug identifier.	xclerc
2013-09-20	Execute tests from the "bugs/closed" directory.	xclerc
2013-09-20	Update test for bug 2846 in order to use "Fail".	xclerc
2013-09-20	Use "Fail" rather than rely on exit code.	xclerc
2013-09-19	Uminus.v : prepare this test file for the use of Fail	letouzey
2013-09-19	universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes	letouzey
2013-09-19	Prettyp: avoid useless "let module"	letouzey
2013-09-19	Made the filename of compiled files explicit, i.e. add a ./ prefix	ppedrot
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-09-18	Removing the last global evar generation in Term_dnet. The very	ppedrot
2013-09-18	Removing unused code from Term_dnet.	ppedrot
2013-09-18	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot
2013-09-18	Taming the simpl evar hack that used to use negative evars.	ppedrot
2013-09-14	Slightly more compact representation of 'a substituted type,	ppedrot
2013-09-13	When Coq is reset-initialed by CoqIDE, do reset jobs counters	gareuselesinge
2013-09-13	fix error reporting window size calculation	gareuselesinge
2013-09-13	CoqIDE: new async error reporting window and slaves status	gareuselesinge
2013-09-13	STM pretty printer should never fail	gareuselesinge
2013-09-13	fix STM feeback on running jobs	gareuselesinge
2013-09-13	Do no compage wg_Notebook terms with (=)	gareuselesinge
2013-09-12	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot
2013-09-12	CoqIDE: show number of proofs being checked in background	gareuselesinge
2013-09-12	Minimal implementation of `Shallow marshalling of Lib	gareuselesinge
2013-09-12	Unknown commands starting a proof were not setting the proof mode.	gareuselesinge
2013-09-12	Remove outdated comment	gareuselesinge
2013-09-12	VernacList handling was lost in STM merge	gareuselesinge
2013-09-12	Fix bug in CStack introduced by refactoring	gareuselesinge
2013-09-10	Temporary fix of emacs mode for ProofGeneral	letouzey
2013-09-07	Change syntax of Hint Resolve to actually accept user-given priorities.	msozeau
2013-09-06	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot
2013-09-05	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot
2013-09-05	Documentation of Evd.	ppedrot
2013-09-05	Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.	ppedrot
2013-09-04	More robust argument setter in CoqIDE. It does not crash anymore on bad	ppedrot
2013-09-03	Fixing some tests from the test-suite.	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-09-03	Some cleanup in Auto	ppedrot
2013-09-02	Removing more association lists in Constrintern.	ppedrot
2013-09-02	* test-suite/success/Unicode_utf8:	regisgia
2013-09-02	* lib/Unicode:	regisgia
2013-09-02	* parsing/Lexer: Cosmetics.	regisgia