coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-03-08	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-05	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin
2006-02-27	dp: sortie Why	filliatr
2006-02-22	Add vernacular file for subtac	coq
2006-02-20	Forgot a file	coq
2006-02-20	Change in subtac modules	coq
2006-02-12	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin
2006-02-08	Julien:	bertot
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-04	code mort	herbelin
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq
2006-01-31	Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char	herbelin
2006-01-16	dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmo	letouzey
2006-01-04	Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...	herbelin
2005-12-30	Correction dépendance g_prim.ml4/q_coqast.ml4	herbelin
2005-12-26	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-25	Utilisation de -notop pour imposer l'absence de module toplevel	herbelin
2005-12-23	Débranchement des parseurs de syntaxe v7	herbelin
2005-12-20	Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...	herbelin
2005-12-15	correction d'un bug dans le make install	narboux
2005-12-02	Changement des named_context	gregoire
2005-11-18	commited new ring	barras
2005-11-07	Adds tools to help in defining new general recursive functions	bertot
2005-11-05	option -w y finalement pas admise par ocamlc <= 3.08.2	herbelin
2005-11-04	Compatibilité ocaml 3.09	herbelin
2005-08-17	new congruence	corbinea
2005-07-15	Subtac: traitement correct des existentielles et de la rÃ©cursion.	coq
2005-07-15	reflexive tauto	corbinea
2005-06-24	dp: ajout des prédicats de sortes	coq
2005-06-09	dp: traitement des fixpoints	coq
2005-05-25	Forgot to remove a cmo.	coq
2005-05-25	Added subtac contrib.	coq
2005-05-24	dp: ajout du prouveur Zenon	coq
2005-05-20	Interface vers outil de recherche Whelp	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin