coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey	2006-04-29
*	Suppression de l'entrée devdoc dans le Makefile principal et modification en...	notin	2006-04-27
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
*	reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / Ordere...	letouzey	2006-03-28
*	Correction d'un bug sur 'make doc' et modification des propriétés dans doc/	notin	2006-03-23
*	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-22
*	Bug BYTEFLAGS pour compilation bin/parser	herbelin	2006-03-18
*	ajout d'un debut de proprietes pour les FSetWeak	letouzey	2006-03-17
*	Ajout de theories/FSets contenant la partie "light" de FSets et FMap:	letouzey	2006-03-15
*	r8637@thot: notin \| 2006-03-14 16:00:49 +0100	notin	2006-03-14
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	r8623@thot: notin \| 2006-03-08 12:40:57 +0100	notin	2006-03-08
*	r8620@thot: notin \| 2006-03-08 11:44:16 +0100	notin	2006-03-08
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	dp: sortie Why	filliatr	2006-02-27
*	Add vernacular file for subtac	coq	2006-02-22
*	Forgot a file	coq	2006-02-20
*	Change in subtac modules	coq	2006-02-20
*	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin	2006-02-12
*	Julien:	bertot	2006-02-08
*	Ajout bibliothèque String de Laurent Théry	herbelin	2006-02-08
*	code mort	herbelin	2006-02-04
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01
*	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin	2006-01-31
*	dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmo	letouzey	2006-01-16
*	Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...	herbelin	2006-01-04
*	Correction dépendance g_prim.ml4/q_coqast.ml4	herbelin	2005-12-30
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Achèvement suppression traducteur dans contrib/interface	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Utilisation de -notop pour imposer l'absence de module toplevel	herbelin	2005-12-25
*	Débranchement des parseurs de syntaxe v7	herbelin	2005-12-23
*	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin	2005-12-20
*	correction d'un bug dans le make install	narboux	2005-12-15
*	Changement des named_context	gregoire	2005-12-02
*	commited new ring	barras	2005-11-18
*	Adds tools to help in defining new general recursive functions	bertot	2005-11-07
*	option -w y finalement pas admise par ocamlc <= 3.08.2	herbelin	2005-11-05
*	Compatibilité ocaml 3.09	herbelin	2005-11-04
*	new congruence	corbinea	2005-08-17
*	Subtac: traitement correct des existentielles et de la rÃ©cursion.	coq	2005-07-15
*	reflexive tauto	corbinea	2005-07-15
*	dp: ajout des prédicats de sortes	coq	2005-06-24
*	dp: traitement des fixpoints	coq	2005-06-09
*	Forgot to remove a cmo.	coq	2005-05-25
*	Added subtac contrib.	coq	2005-05-25
*	dp: ajout du prouveur Zenon	coq	2005-05-24