coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-07	- per session coq command stack	vgross
2009-03-06	fixed groebner as a plugin + pattern matching Timeout	barras
2009-03-04	Temporary hack to make coqide.byte work (backport r11948) (see #2062)	glondu
2009-02-11	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin
2009-01-17	DISCLAIMER	puech
2009-01-06	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-10-28	Native "Declare ML Module" when possible	glondu
2008-10-03	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau
2008-07-18	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin
2008-07-10	Bug résiduel du backtrack de coqide se produisant lorsque la limite de	herbelin
2008-07-01	Encore une suite au 11188/11193 (c'était pas un bon jour)	herbelin
2008-06-13	CoqIDE: 2 problèmes de undo encore:	herbelin
2008-06-11	Plutôt que de reposer sur le vernacexpr pour détecter les débuts de	herbelin
2008-06-09	On prend des risques en tentant d'optimiser encore plus le undo en cas	herbelin
2008-06-06	- On adopte finalement la méthode de Pierre Courtieu pour le undo de	herbelin
2008-05-30	- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"	herbelin
2008-05-28	Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image de	herbelin
2008-05-26	Réorganisation des points d'appui du undo de CoqIDE (type reset_info).	herbelin
2008-05-26	Bug undo CoqIDE sur End	herbelin
2008-05-25	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin
2008-05-24	- Prise en compte des frozen state de Coq autant que possible pour	herbelin
2008-05-20	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin
2008-05-10	Amélioration de la colorisation, du backtrack et des messages de CoqIDE	herbelin
2008-05-08	Efficacité, bugs, robustesse CoqIDE	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-10-16	add visibility of extraction messages in coqide	letouzey
2007-10-04	Bug 1716: Scheme now print the right messages	vsiles
2007-04-26	fin des conclusions multiples	corbinea
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-01-25	decl mode: anonymous facts	corbinea
2006-10-23	fixed same_file (#1141)	barras
2006-10-19	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-01	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin
2006-07-28	Modifications dans les scripts de configuration (coqtop et coqide affichent m...	notin
2006-07-06	Remplacement VernacDebug par VernacSetOption (suite)	herbelin
2006-06-07	Changement de l'option -where: on vérifie si la variable d'environnement COQ...	notin
2006-05-30	Correction bug #990 (LoadPath et option -R de coqide	notin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-11-23	bug de coqide sous windows (bad file descriptor)	barras
2005-11-02	Types inductifs parametriques	mohring
2005-01-06	- Module/Declare Module syntax made more uniform:	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-03-03	ide: silent behavior better, save icon, -byte works	marche
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin