coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	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
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot	2013-12-22
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-10
*	Revert the previous commit. It broke Coq compilation.	ppedrot	2013-11-09
*	Removing the dependency of every level of tactic ATSs on glob_tactic_expr.	ppedrot	2013-11-09
*	STM: fix for PG and "Proof term" lines.	gareuselesinge	2013-11-05
*	Adds an experimental exactly_once tactical.	aspiwack	2013-11-02
*	Adds a tactical once.	aspiwack	2013-11-02
*	Added the tactical "tac1 + tac2".	aspiwack	2013-11-02
*	Fixes parsing of all: followed by a typechecking/evaluation command.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	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
*	STM: better handle proof modes	gareuselesinge	2013-09-30
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
*	stm: (initial) support for -coq-slaves	gareuselesinge	2013-08-08
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge	2013-08-08
*	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
*	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
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Getting rid of IntroPatternArgType.	ppedrot	2013-06-27
*	Removing useless tactic arguments, and using generic arguments	ppedrot	2013-06-27
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	More comments in Genarg.	ppedrot	2013-06-06
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05
*	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
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Useless use of hooks in VernacDefinition. In addition, this was	ppedrot	2013-02-10
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22