coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	config/revision.ml, git: handle case when not at tip of a branch	lmamane	2009-02-11
*	clean: revision is now called config/revision.ml	lmamane	2009-02-11
*	Convert all uses of FIND_VCS_CLAUSE to recommended style	lmamane	2009-02-11
*	Cyclic31: proof of a forgotten admit	letouzey	2009-02-10
*	removed prehistoric files	barras	2009-02-10
*	man page of coqchk	barras	2009-02-10
*	Correction bug coqdev Hermann lehener.	soubiran	2009-02-10
*	commited complexity test for exponential behavior of unification	barras	2009-02-09
*	memoized is_ground_env	barras	2009-02-09
*	pushed evar reduction in kernel	barras	2009-02-06
*	Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]	herbelin	2009-02-06
*	Fixing #2044 (bad printing of primitive notation at the head of	herbelin	2009-02-06
*	From v8.2 to trunk:	herbelin	2009-02-06
*	Fix [subrelation] clauses that privileged the weakest. Better impl args	msozeau	2009-02-04
*	Report r11631 from 8.2 and handle non-dependent goals better in	msozeau	2009-02-04
*	Fix d'un bug avec l'option gallina	notin	2009-02-04
*	Do not reserve the keyword "Infer".	puech	2009-02-03
*	Allow to turn contrib/subtac into a (nat)dynlink'able plugin	letouzey	2009-02-03
*	Fix the installation of plugins (both initial and late ones)	letouzey	2009-02-03
*	Reorder coqmktop options and document -echo	glondu	2009-01-31
*	More portable way to pipe stderr	glondu	2009-01-30
*	Correction bug 2037.	soubiran	2009-01-30
*	Solves some warning and hides some not-bad ones in doc. It remains a	herbelin	2009-01-29
*	FSet(Weak)List : eq_dec becomes Defined (and gets better proof)	letouzey	2009-01-28
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).	herbelin	2009-01-27
*	Forgot a file in r11859. Sorry...	puech	2009-01-27
*	Revert changes in pcoq functions to restore compatibility with contribs	puech	2009-01-26
*	Suppression de l'ancien logo (problèmes de droits)	notin	2009-01-23
*	Really compare evar maps in progress, due to merging in apply and other	msozeau	2009-01-23
*	Petit nettoyage faisant suite au commit #11847 .	aspiwack	2009-01-23
*	Fix #2011 : an incorrect environment when extracting Module ... with ...	letouzey	2009-01-22
*	Util.split_at : for quadratic to linear complexity	letouzey	2009-01-22
*	Extraction Library works now when some files share the same short name (fix #...	letouzey	2009-01-22
*	Fixes in the documentation of [dependent induction] and test-suite	msozeau	2009-01-22
*	configure: more adequate message explaining what -opt is doing	letouzey	2009-01-22
*	Fix d'un petit problème avec ocamlmklib en présence de l'option -camldir	notin	2009-01-22
*	Remplacement de cp --parents par un script sh	notin	2009-01-22
*	Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824	herbelin	2009-01-21
*	Fix bug #2004 due to bad handling of evars in the unification for	msozeau	2009-01-21
*	- Better deal with commands inside section titles in latex output using	msozeau	2009-01-21
*	Fixing bug #1918 (no occur-check in Meta unification was done yet!).	herbelin	2009-01-20
*	- Fixing bug 1891 (abusive instantiations of evar arguments in	herbelin	2009-01-20
*	Fixing a bug in 11804 (support for _ in ident entry of notations).	herbelin	2009-01-20
*	Added some missing statements for proof folding and corrected	vgross	2009-01-20
*	Added proof folding into CoqIde. See RefMan for using it.	vgross	2009-01-20
*	Cette version là fonctionne correctement au moins pour certaines	aspiwack	2009-01-20
*	More fixes...	aspiwack	2009-01-20
*	Un fix sur le commit précédent.	aspiwack	2009-01-20
*	Patch de l'installation:	aspiwack	2009-01-20