coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Array.create is deprecated	pboutill	2012-12-19
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Fix typo	glondu	2012-01-12
*	Nsatz: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	nsatz ajoute	pottier	2010-06-03