coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi	2014-10-13
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
*	Factorize the parsing rules of [Record] and the other kind of type definitions.	Arnaud Spiwack	2014-09-04
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack	2014-09-04
*	Fixing bug #3493.	Pierre-Marie Pédrot	2014-08-27
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	Adding a new "Locate Term" command, distinct from the raw "Locate" command.	Pierre-Marie Pédrot	2014-07-21
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a Print Strategy vernacular command. It allows to check the	Pierre-Marie Pédrot	2014-03-19
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	Documenting old but useful command "Print Tables".	Hugo Herbelin	2014-01-13
*	Fixing bug #3144.	Pierre-Marie Pédrot	2014-01-10
*	Patch for supporting [From Xxx Require Yyy Zzz.]	Gregory Malecha	2013-12-12
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	New option Default Goal Selector.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	STM: add "Stm Wait" to wait for the slaves to complete their jobs	gareuselesinge	2013-10-10
*	STM: new command "Stm PrintDag" to force printing the dag to /tmp	gareuselesinge	2013-10-07
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	Support Proof General	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	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
*	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
*	Fixing warning of deprecated Argument Scopes.	ppedrot	2013-05-28
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	More functional implementation of locality_flag and program_mode	gareuselesinge	2013-04-15
*	Modules and ppvernac, sequel of Enrico's commit 16261	letouzey	2013-03-13
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10