coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing useless use of metaids in tactic AST.	Pierre-Marie Pédrot	2014-05-22
*	Removing decompose record / sum from the tactic AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving left & right tactics out of the AST.	Pierre-Marie Pédrot	2014-05-21
*	Moving (e)transitivity out of the AST.	Pierre-Marie Pédrot	2014-05-20
*	Tentative to add constr-using primitive tactics without grammar rules.	Pierre-Marie Pédrot	2014-05-20
*	Adding way to get the list of the accepted tactic notation arguments.	Pierre-Marie Pédrot	2014-05-17
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Moving the ML tactic extension mechanism to a Libobject-based one.	Pierre-Marie Pédrot	2014-05-12
*	Cleanup before merge with the trunk	Matthieu Sozeau	2014-05-06
*	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
*	Closing bug #3260	Julien Forest	2014-04-14
*	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
*	Migrate back g_obligations in toplevel	Pierre Letouzey	2014-03-02
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	G_xml: remove some duplication in error fonctions	Pierre Letouzey	2014-01-30
*	G_xml: protect against some possible Not_found	Pierre Letouzey	2014-01-30
*	Documenting old but useful command "Print Tables".	Hugo Herbelin	2014-01-13
*	Fixing bug #3144.	Pierre-Marie Pédrot	2014-01-10
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Patch for supporting [From Xxx Require Yyy Zzz.]	Gregory Malecha	2013-12-12
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
*	Actually adding the grammar entry to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	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
*	Moving notation types into grammar rule.	ppedrot	2013-11-09
*	Cleaning and documenting Egramcoq.	ppedrot	2013-11-09
*	empty token in terminal is a user error not an anomaly (bug 3118)	pboutill	2013-11-03
*	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
*	New option Default Goal Selector.	aspiwack	2013-11-02
*	Adds a new goal selector "all:".	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	Removing some generic equalities.	ppedrot	2013-10-22
*	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
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27