coq - The formal proof system

Age	Commit message (Expand)	Author
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
2013-08-30	Stm: if slave process dies badly go back to local lazy evaluation	gareuselesinge
2013-08-30	-coq-slaves: close_on_exec + correct argument passing	gareuselesinge
2013-08-30	Remove Obj.magic from safe typing	gareuselesinge
2013-08-30	Trickyer test for Paral-ITP	gareuselesinge
2013-08-28	Fixing bug #3083.	ppedrot
2013-08-28	Removing some lone List.assoc & List.mem in lib.	ppedrot
2013-08-25	Removing association lists in Reductionops. Btw, defining the dual of the	ppedrot
2013-08-25	Actually using the domain function for maps.	ppedrot
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-08-23	Adding dynamic value printing to votour through a registering mechanism.	ppedrot
2013-08-23	Fix computation of discharged hyps for inductive types forgetting the conclus...	msozeau
2013-08-23	Updating documentation of the ring/field tactics.	amahboub