coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Useless hooks in Tacintern.	Pierre-Marie Pédrot	2014-09-03
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Centralizing the Ltac-defining functions in Tacenv.	ppedrot	2013-11-10
*	Replacing an association list by a map in globalizing environment.	ppedrot	2013-08-03
*	Removed the distinction between generic Ltac vars and Let/Intro	ppedrot	2013-06-27
*	Splitted up Genarg in four different levels:	ppedrot	2013-06-21
*	Removing the various glob/subst/interp registering functions for	ppedrot	2013-06-18
*	Now glob_sign and interp_sign only depend on structures defined	ppedrot	2013-06-18
*	Make ist (interp_sign) available to TACTIC EXTEND code	gareuselesinge	2013-05-29
*	Modulification of identifier	ppedrot	2012-12-14
*	Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp	letouzey	2012-10-16