coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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 almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
*	STM pretty printer should never fail	gareuselesinge	2013-09-13
*	fix STM feeback on running jobs	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
*	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
*	Temporary fix of emacs mode for ProofGeneral	letouzey	2013-09-10
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	summary for ML modules made correct	gareuselesinge	2013-08-30
*	Make the jopin-document button wait for slaves to terminate	gareuselesinge	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
*	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
*	Fixing bug #3083.	ppedrot	2013-08-28
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Misc changes around coqtop.ml :	letouzey	2013-08-22
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	Fix STM: Module Import may change the parser	gareuselesinge	2013-08-20
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Himsg : strict 80-column indentation	letouzey	2013-08-20
*	Safe_typing code refactoring	letouzey	2013-08-20
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	Modulification and removing of structural equality in VCS.	ppedrot	2013-08-19
*	Fixing potentially misused Errors.push.	ppedrot	2013-08-12
*	Mutual proofs cannot be delegated	gareuselesinge	2013-08-11
*	Small typos	ppedrot	2013-08-10
*	Lemmas ending with Defined cannot be delegated to slaves	gareuselesinge	2013-08-10
*	Fix batch compilation of scripts with Admitted proofs (in a section)	gareuselesinge	2013-08-09
*	fix batch compilation of scripts containing Admitted	gareuselesinge	2013-08-09
*	stm: (initial) support for -coq-slaves	gareuselesinge	2013-08-08
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	enhance marshallable option for freeze (minor TODO in safe_typing)	gareuselesinge	2013-08-08
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	Simple machinery to detect EXTEND that interpret during parsing	gareuselesinge	2013-08-08
*	Support Proof General	gareuselesinge	2013-08-08
*	Coqide ported to STM	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Added more flags choice in desambiguating printer. The code is	ppedrot	2013-08-06
*	Tentative fix for bug #2961. When we have to print two terms that	ppedrot	2013-08-05
*	Fixing #2846: Uncaught exception Reduction.NotArity.	ppedrot	2013-08-04
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Replacing uses of association lists by maps in notations.	ppedrot	2013-08-03
*	Small typo in Print Debug GC	ppedrot	2013-08-02