coq - The formal proof system

Age	Commit message (Expand)	Author
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-06-27	Getting rid of IntroPatternArgType.	ppedrot
2013-06-27	Removing useless tactic arguments, and using generic arguments	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-06	More comments in Genarg.	ppedrot
2013-02-19	Dir_path --> DirPath	letouzey
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-16	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey
2012-10-06	remove useless hidden_flag in TacMutual(Co)Fix	letouzey
2012-10-06	Tacexpr: revised version that doesn't need -rectypes	letouzey
2012-10-01	Added a new tactical infoH tac, that displays the names of hypothesis created...	courtieu
2012-08-08	Updating headers.	herbelin
2012-07-09	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-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	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