coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot	2014-07-25
*	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack	2014-07-24
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	Moving the [split] tactic out of the AST.	Pierre-Marie Pédrot	2014-06-06
*	Moving the "specialize" tactic out of the AST. Also removed an obsolete	Pierre-Marie Pédrot	2014-05-22
*	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
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	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
*	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
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	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
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16
*	remove useless hidden_flag in TacMutual(Co)Fix	letouzey	2012-10-06
*	Tacexpr: revised version that doesn't need -rectypes	letouzey	2012-10-06
*	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu	2012-10-01
*	Updating headers.	herbelin	2012-08-08
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
*	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey	2012-05-29