coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Getting rid of module Gmapl.	ppedrot	2013-05-09
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Uniformization: isevars -> evdref/sigma/evd	herbelin	2013-05-09
*	Fixing r16487 on sharing evars between multiple parameters (missing List.rev).	herbelin	2013-05-09
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Declaration of multiple hypotheses or parameters now share typing	herbelin	2013-05-08
*	Share more information between constructors and arity of an inductive	herbelin	2013-05-08
*	New module Xml_printer (dual to Xml_parser)	gareuselesinge	2013-05-06
*	States: frozen states can hold closures	gareuselesinge	2013-05-06
*	Close the .glob file after having saved .vo	gareuselesinge	2013-05-06
*	Improvement of r16204 on reporting tactic error locations: if the main	herbelin	2013-05-05
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Fix compilation (vernac.ml, missing ;)	gareuselesinge	2013-04-25
*	Flag ide_slave moved into Flags module	gareuselesinge	2013-04-25
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
*	Coqide: new feedback mechanism for structured content	gareuselesinge	2013-04-25
*	Fix issues with "Reset Initial" in scripts given to coqtop -l	letouzey	2013-04-23
*	minor cleanup in coqtop.ml	letouzey	2013-04-23
*	coqtop -compile: avoid with_heavy_rollback when non-interactive	letouzey	2013-04-23
*	Coqtop -compile : avoid saving init state when compiling just one file	letouzey	2013-04-23
*	Remove deprecated option -no-hash-consing (currently doing nothing)	letouzey	2013-04-23