coq - The formal proof system

Age	Commit message (Expand)	Author
2013-09-30	fake_ide: call Coq.init as the first action	gareuselesinge
2013-09-30	ideutils: stock_to_widget was ignoring the ~size argument	gareuselesinge
2013-09-30	wg_Command: detachable, less "from the 80s", query pane	gareuselesinge
2013-09-30	wg_Session: fix copy/paste of tagged text	gareuselesinge
2013-09-30	STM: some refactoring, support revised CoqIDE protocol	gareuselesinge
2013-09-30	CoqIDE ported to the revides protocol	gareuselesinge
2013-09-30	fake_ide ported to the new protocol (FIXME tests fail)	gareuselesinge
2013-09-30	CoqIDE protocol/serialization revised	gareuselesinge
2013-09-30	lib/cstack: various improvements	gareuselesinge
2013-09-30	lib/vcs: various improvements	gareuselesinge
2013-09-30	lib/dag: various improvements	gareuselesinge
2013-09-30	lib/future: computations that are Exn can be replaced	gareuselesinge
2013-09-28	Made rewrite tactic strategies pure. They were using quite uglily	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-26	Opacifying the type of strategies.	ppedrot
2013-09-26	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot
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