coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Added a Print Debug GC command that displays the current state of	ppedrot	2013-08-01
*	Granting bug #3098: adding priority to Existing Instances.	ppedrot	2013-08-01
*	better error message for unexpected renaming (closes #2987)	gareuselesinge	2013-07-29
*	Revert "Only arguments declared as implicit can be renamed"	gareuselesinge	2013-07-29
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	Added a Register Inline command for the native compiler. Will be ported to th...	mdenes	2013-07-10
*	Removing the use of leveled tactics wit_tacticn. It is now handled	ppedrot	2013-07-02
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Fixing bug #3030.	ppedrot	2013-06-06
*	More comments in Genarg.	ppedrot	2013-06-06
*	Add an option to shrink the context of program obligations to avoid	msozeau	2013-06-06
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	Making the behavior of "injection ... as ..." more natural:	herbelin	2013-06-02
*	Removing a useless location in ltac trace mechanism.	ppedrot	2013-05-30
*	Getting rid of LtacLocated exception transformer.	ppedrot	2013-05-28
*	Replacing Id.check with Id.is_valid, as its sole use was under	ppedrot	2013-05-14
*	Use the Hook module here and there.	ppedrot	2013-05-12
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09