coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Do not install csdpcert in $(BINDIR)	glondu	2008-09-07
*	Install coqide manpage	glondu	2008-09-06
*	More cleaning	glondu	2008-09-06
*	Use $(COQTOPEXE) to refer to bin/coqtop in Makefiles	glondu	2008-09-06
*	Build coqrun library using ocamlmklib...	glondu	2008-09-05
*	Initial implementation of a new command to define (dependent) functions by	msozeau	2008-09-02
*	added Makefile target: validate (to recheck all .vo in a row)	barras	2008-09-02
*	Renaming parser -> coq-parser	glondu	2008-08-18
*	Install csdpcert with libraries	glondu	2008-08-16
*	micromega : bug fixes and optimisations	fbesson	2008-08-07
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Now, -browser option is effective (and compiles)	glondu	2008-07-27
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
*	Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, re...	notin	2008-07-16
*	Micromega: doc + test-suite update	fbesson	2008-07-07
*	Some work on BigQ :	letouzey	2008-06-25
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin	2008-06-25
*	Report de la révision #11175 de la branche v8.2 vers le trunk	notin	2008-06-25
*	Micromega : bugs fixes - renaming of tactics - documentation	fbesson	2008-06-25
*	Suppression de l'option -dump-glob et ajout d'une option -no-glob	notin	2008-06-24
*	Remplacement des 'cp' et 'mkdir' par 'install'	notin	2008-06-12
*	2-3 petites modifs pour la compilation sous Windows...	notin	2008-06-06
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
*	In abstract parts of theories/Numbers, plus/times becomes add/mul,	letouzey	2008-06-03
*	Quelques amendements liées à la compilation des packages.	herbelin	2008-06-01
*	BigQ: starting to create and use an interface QSig	letouzey	2008-06-01
*	Enhance the BigN and BigZ infrastructure:	letouzey	2008-06-01
*	NBigN: proofs that BigN implements axioms of NAxiomsSig	letouzey	2008-05-29
*	Cyclic31 : proof of the spec of gcd31	letouzey	2008-05-27
*	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
*	added coqchk to the main Makefile and a make variable VALIDATE to check the v...	barras	2008-05-22
*	Intégration de micromega ("omicron" pour fourier et sa variante sur Z,	herbelin	2008-05-19
*	ZModulo: Z viewed modulo 2^digits implements CyclicAxioms	letouzey	2008-05-17
*	Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate	letouzey	2008-05-16
*	BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZ	letouzey	2008-05-16
*	ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.	letouzey	2008-05-16
*	More BigNum cleanup:	letouzey	2008-05-16
*	Oubli lors de la révision 10899 (Bool_nat.vo)	notin	2008-05-15
*	Still Ints-->Numbers transition: fix the previous commit about a typo	letouzey	2008-05-09
*	Still Ints-->Numbers transition: fix a typo preventing the compilation of BigQ	letouzey	2008-05-08
*	Integration of theories/Ints into theories/Numbers, part 1: moving files	letouzey	2008-05-07
*	menage dans funind + deplaceemnt de recdef dans funind	jforest	2008-04-28
*	Suite r10857	herbelin	2008-04-27
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Addded the "Dump Tree" command.	cek	2008-04-21
*	tactique gappa	filliatr	2008-04-17
*	Add almost empty Classes.tex for documentation of type classes.	msozeau	2008-04-17
*	first-order --> firstorder (kills a warning about not being a valid id)	letouzey	2008-04-16
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08