coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Splitting the nsatz ML module into an implementation and a grammar files.	Pierre-Marie Pédrot	2016-03-06
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Fixing an incompleteness of the ring/field tactics	amahboub	2013-08-23
*	Little fix for Nsatz: hypotheses not directly relevant to the nsatz	herbelin	2013-05-05
*	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey	2013-03-13
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Array.create is deprecated	pboutill	2012-12-19
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	More cleanup in Ring_polynom and EnvRing	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Cleaning opening of the standard List module.	ppedrot	2012-06-28
*	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
*	moins de reification inutile, noatations standards	pottier	2011-08-04
*	Nsatz: replaced some generic = on constr by eq_constr	puech	2011-07-29
*	Ring2 devient Ncring et la reification par les type classes est partagee	pottier	2011-07-26
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
*	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
*	Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits	letouzey	2010-11-18
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier	2010-07-28
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...	pottier	2010-07-28
*	nstaz pour les anneaux integres et les setoides, R Z et Q	pottier	2010-07-27
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Fix compilation and test-suite of nsatz	glondu	2010-07-12
*	nsatz in an integral domain with specialization to Z and R	pottier	2010-07-08
*	bug 2328 fixed: failure when polynomial not i ideal	pottier	2010-06-25
*	Misc fixes related to new nsatz (and ocamlbuild)	letouzey	2010-06-03
*	nsatz ajoute	pottier	2010-06-03