coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Opacifying the type of strategies.	ppedrot	2013-09-26
*	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot	2013-09-26
*	Removing useless evar-related stuff.	ppedrot	2013-09-25
*	Adding evar printing to debugger.	ppedrot	2013-09-24
*	Fixing ocamldebug compilation by adding thread linking.	ppedrot	2013-09-24
*	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-20
*	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-19
*	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-18
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
*	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-13
*	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-12
*	Temporary fix of emacs mode for ProofGeneral	letouzey	2013-09-10
*	Change syntax of Hint Resolve to actually accept user-given priorities.	msozeau	2013-09-07
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	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-05
*	More robust argument setter in CoqIDE. It does not crash anymore on bad	ppedrot	2013-09-04
*	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-03
*	Removing more association lists in Constrintern.	ppedrot	2013-09-02