coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	A file that can be loaded when a migration from Set to Type is desired	letouzey	2008-04-04
*	New file FMapFullAVL containing the balancing proofs about FMapAVL:	letouzey	2008-04-03
*	Various fixes on typeclasses:	msozeau	2008-03-27
*	Installation des .vo nécessaire à BigQ	notin	2008-03-20
*	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey	2008-03-19
*	Ajout cible programs comme synonyme de subtac	herbelin	2008-03-16
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)	letouzey	2008-03-15
*	tactique Gappa : mise en place	filliatr	2008-03-11
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Merge with lmamane's private branch:	lmamane	2008-02-22
*	Petits oublis dans Makefile.doc	notin	2008-02-20
*	Plongement de doc/Makefile dans la nouvelle architecutre des Makefile	notin	2008-02-14
*	Move class_setoid to class_tactics.	msozeau	2008-02-13
*	New algorithm to resolve morphisms, after discussion with Nicolas	msozeau	2008-02-06
*	Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps	letouzey	2008-02-04
*	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau	2008-02-03
*	factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...	letouzey	2008-02-02
*	Prove the decidability of arithmetical statements using the real numbers.	roconnor	2008-01-24
*	Fix Makefile bug, using .v instead of .vo and document SetoidDec.v	msozeau	2008-01-17
*	Bug in sqrt321	thery	2008-01-17
*	Amélioration de la génération des graphes de dépendances	notin	2008-01-11
*	Add partial setoids in theories/Classes, add SetoidDec class for setoids with...	msozeau	2008-01-04
*	Move Classes.Setoid to Classes.SetoidClass to avoid name clash.	msozeau	2007-12-31
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Correction du bug #1745 (installation des fichiers .vo de Numbers)	notin	2007-12-18
*	migration of ide/utf8.v to theories/Unicode/Utf8.v	letouzey	2007-12-13
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Added theorems; created NZPlusOrder from NTimesOrder.	emakarov	2007-11-16
*	Split NTimesOrder into properly NTimesOrder and NPlusOrder.	emakarov	2007-11-15
*	Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...	emakarov	2007-11-14
*	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey	2007-11-08
*	Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.	emakarov	2007-11-07
*	Replaced BinNat with a new version that is based on theories/Numbers/Natural/...	emakarov	2007-11-07
*	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey	2007-11-06
*	Adding Qround.v (and helper lemmas and hints)	roconnor	2007-11-01
*	Adding BigQ and proofs	thery	2007-10-25
*	Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to u...	emakarov	2007-10-25