coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	fixed bug #1780: a lift was missing (match predicate)	barras	2008-05-29
*	NBigN: proofs that BigN implements axioms of NAxiomsSig	letouzey	2008-05-29
*	- Modification de la déf de minus et pred conformément aux remarques de	herbelin	2008-05-28
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are	letouzey	2008-05-28
*	CyclicAxioms: after discussion with Laurent, znz_WW and variants are	letouzey	2008-05-28
*	replace the query window of coqide by a pane in main window as suggested by hugo	jnarboux	2008-05-28
*	introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...	barras	2008-05-28
*	add option to change modifiers of display menu	jnarboux	2008-05-28
*	update gtk requirements	jnarboux	2008-05-28
*	Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image de	herbelin	2008-05-28
*	add support for pdf in coqdoc, add export to pdf in coqide, port open and sav...	jnarboux	2008-05-28
*	debug : case where length of s is < 2...	jnarboux	2008-05-28
*	- Correction bug highlighting "Module" dans Coqide	herbelin	2008-05-28
*	Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !	letouzey	2008-05-28
*	Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...	letouzey	2008-05-27
*	Correction du problème de complexité de Print Assumptions :	aspiwack	2008-05-27
*	add install instruction for mandriva	jnarboux	2008-05-27
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	update changes related to coqide	jnarboux	2008-05-27
*	Cyclic31 : proof of the spec of gcd31	letouzey	2008-05-27
*	revert toolbar to previous state: icons style	jnarboux	2008-05-27
*	Int31 : gcd31 was wrong	letouzey	2008-05-26
*	remove set printing ... and unset printing ... from template menu as they are...	jnarboux	2008-05-26
*	Cyclic31: cleanup, 2 Admitted killed (6 remaining)	letouzey	2008-05-26
*	transform the toolbar icons for display of information into a Display menu wi...	jnarboux	2008-05-26
*	debug subst_command_placeholder : replace %s and not only %	jnarboux	2008-05-26
*	Réorganisation des points d'appui du undo de CoqIDE (type reset_info).	herbelin	2008-05-26
*	Encore un bug de undo	herbelin	2008-05-26
*	Résolution bug #1850 sur notations avec niveaux inconnus de	herbelin	2008-05-26
*	Fix bashism in doc generation.	glondu	2008-05-26
*	Bug undo CoqIDE sur End	herbelin	2008-05-26
*	the -g option is not recongnized in ocaml < 3.10.0	jforest	2008-05-26
*	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin	2008-05-25
*	- Prise en compte des frozen state de Coq autant que possible pour	herbelin	2008-05-24
*	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin	2008-05-24
*	doc of coqchk + improved module cache and computation of module sets	barras	2008-05-23
*	Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...	letouzey	2008-05-23
*	- Fix bug #1858, Hint Unfold calling the wrong locate function.	msozeau	2008-05-23
*	Nouvelle doc pour les modules.	soubiran	2008-05-23
*	(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...	letouzey	2008-05-23
*	Strategy commands are now exported	barras	2008-05-22
*	fixed dependency problems with the checker	barras	2008-05-22
*	writing a match on a digit via syntax "if ... then ... else" is not a good id...	letouzey	2008-05-22
*	Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...	letouzey	2008-05-22
*	QRewrite is now obsolete. It was containing manual ltac stuff	letouzey	2008-05-22
*	Should fix the dependancy issue mentioned by J.Forest about NMake:	letouzey	2008-05-22
*	switch theories/Numbers from Set to Type (both the abstract and the bignum pa...	letouzey	2008-05-22
*	improved coqchk targets	barras	2008-05-22
*	added coqchk to the main Makefile and a make variable VALIDATE to check the v...	barras	2008-05-22