coq - The formal proof system

Age	Commit message (Expand)	Author
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
2013-09-02	* configure: Remove trailing space.	regisgia
2013-08-30	summary for ML modules made correct	gareuselesinge
2013-08-30	add "Print Ring" and "Print Field" vernacular commands	gareuselesinge
2013-08-30	Make the jopin-document button wait for slaves to terminate	gareuselesinge
2013-08-30	Fixing the code of field_simplify_eq.	amahboub
2013-08-30	When PG is used as interface behave as before STM	gareuselesinge
2013-08-30	ind_tables: properly handling side effects	gareuselesinge
2013-08-30	recdef: restore old semantics (pre STM)	gareuselesinge
2013-08-30	Fix typo in error message	gareuselesinge
2013-08-30	safe Conv_oracle state for type checking	gareuselesinge