coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-28	Prise en compte dépendance de subtyping en typeops (polymorphisme de defs)	herbelin
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-27	Ajout ListTactics	herbelin
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-25	conflit de nom (Field_theory) modulo la casse	barras
2006-10-17	Mise en forme des theories	notin
2006-10-11	Ajout d'une option -annotate au configure+ changement du comportement par dé...	notin
2006-09-28	separation de RealField	barras
2006-09-28	Makefile : COQLIB -> FULLCOQLIB	corbinea
2006-09-26	petits pbs de dependances	barras
2006-09-26	Compilation newring	notin
2006-09-26	commit de field + renommages	barras
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-18	Correction du bug #1215	notin
2006-09-04	Fix wrong order for building library, add informative messages.	msozeau
2006-09-01	Subtac fixes, new way of handling obligations in progress.	msozeau
2006-08-30	Modification du configure pour paramétrer les exécutables liés à la compi...	notin
2006-08-29	Changement de l'appel aux exécutables Caml (noms absolus)	notin
2006-07-28	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin
2006-07-26	Modification script sed pour compatibilité Windows	notin
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2006-07-13	Retrait du -noassert qui etait present en natif.	letouzey
2006-06-25	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey
2006-06-09	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin
2006-06-08	MAJ Makefile depend	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-05-31	ajout de QArith dans les theories standards	letouzey
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-05-26	Modification de la compilation de coqc et coqmktop pour éviter le problème ...	notin
2006-05-22	un debut de propriétés concernant FMap	letouzey
2006-05-18	Dépendances pour List.v	notin
2006-05-16	etoffage des notions de permutations (a la fois List.Permutation et Permutati...	letouzey
2006-05-15	ajout de theories/FSets/DecidableTypeEx.v	letouzey
2006-05-11	Duplication du fichier FSetProperties pour les ensembles Weak.	letouzey
2006-05-04	- intégration de la modification suggérée par L. Mamane: coqmktop passe ma...	notin
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-04-29	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey
2006-04-27	Suppression de l'entrée devdoc dans le Makefile principal et modification en...	notin
2006-04-25	Un gros coup de lifting pour IntMap:	letouzey
2006-04-07	- Documentation of the Program tactics.	msozeau
2006-04-06	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey
2006-03-28	reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...	letouzey
2006-03-23	Correction d'un bug sur 'make doc' et modification des propriétés dans doc/	notin
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-03-22	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin
2006-03-18	Bug BYTEFLAGS pour compilation bin/parser	herbelin
2006-03-17	ajout d'un debut de proprietes pour les FSetWeak	letouzey
2006-03-15	Ajout de theories/FSets contenant la partie "light" de FSets et FMap:	letouzey
2006-03-14	r8637@thot: notin \| 2006-03-14 16:00:49 +0100	notin