coq - The formal proof system

Age	Commit message (Collapse)	Author
2009-03-30	Add a more general quote construction	glondu
	"quote f [...] in c using t" will call t (must be an ltac function) with a X (of form "f x" or "f vm x") such that X converts to c. In particular, match goal with \| H : ?x \|- _ => quote f in x using (fun X => change X in H) end may be used as an equivalent of plain quote that acts on an hypothesis. The construction can be used in a more general way, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12037 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7