coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	commented out overwrite confirmation handler (requires lablgtk >=2.10)	barras	2008-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11019 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵	jnarboux	2008-05-28
\| \| \| \| \| \|	save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1842 + correction bug initialisation introduit dans	herbelin	2008-05-10
\| \| \| \| \| \| \|	commit 10916 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration de la colorisation, du backtrack et des messages de CoqIDE	herbelin	2008-05-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Colorisation: - on ne colorie que les noms de commandes que si en début de phrase (par exemple: Definition F := fun Local => Local) ne colorie pas Local), - ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset sont uniformément mis en valeur). - Backtracking: résolution bug #1538 et réactivation de la possibilité de déclarer des défs, types, etc pendant une session de preuve. En revanche, il n'est pas clair que cela fonctionne bien avec le mode déclaratif. - Messages d'erreur : on ne capture la sortie de coq qu'après l'initialisation pour que les erreurs d'initialisation soit affichées (cf bug #1424 and item 5 of #1123). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Efficacité, bugs, robustesse CoqIDE	herbelin	2008-05-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Suppression d'une source de fuite mémoire dans declare_mod.ml (la table de hash library_table n'était pas synchronisée avec le reset et elle grossissait à chaque rejeu de la session; utilisation au passage d'une map pour que la synchronisation avec le reset soit plus rapide). [mod_typing.ml] - Correction d'un bug de synchronisation pour le niveau pattern 200. [pcoq.ml4] - Suppression d'un vieux reste du traducteur [constructeur VernacVar] - Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de chacune des commandes vernaculaires par l'utilisation d'une fonction d'assignation d'attributs à chaque commande vernac. Correction de ce qui semble être des bizarreries (VernacDeclareTacticDefinition considéré comme ouvrant un but; suppression des "loc" dans les Reset: ne pouvait pas faire fonctionner correctement update_on_end_of_segment). Suppression de la nécessité d'expliciter si une commande retourne des messages dépendants du mode "verbose" (on suppose que chaque commande sait ce qu'elle doit dire selon la position du flag verbose). Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne sait revenir qu'aux états associés à des noms et cela ne vaut pas l'approche de Proof General. Il sera sans doute opportun de se brancher sur l'architecture de Pierre Courtieu à base de "Backtrack". La restriction des buts imbriqués a-t-elle vraiment une raison d'être ? En plus les commandes non cablées en dur comme Next Obligation ne sont pas prises en compte. Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours. Réparation approximative de l'option "Help for Keyword" de Coqide mais encore à faire pour plus de robustesse (makefile, installation, synchronisation entre la version du fichier index_urls.txt et la version du refman, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10904 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
\| \| \| \| \| \| \| \| \|	devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
*	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea	2007-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9566 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed same_file (#1141)	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de l'option -where: on vérifie si la variable d'environnement ↵	notin	2006-06-07
\| \| \| \| \| \|	COQLIB est définie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2005-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7609 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2005-11-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7608 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug de coqide sous windows (bad file descriptor)	barras	2005-11-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7603 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage suite à la détection par défaut des variables inutilisées par ↵	herbelin	2005-11-08
\| \| \| \| \| \|	ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de fonctionnalités unix et browser de ide vers lib	herbelin	2005-05-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	search window	coq	2004-02-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pour ide sous windows	coq	2004-01-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5267 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ameliorations coqide	coq	2003-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide : les nouveaute d'aout	monate	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: warn when using locale or manual charset	monate	2003-07-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide : ported to lablgtk2 snapshot of 2003/07/07	monate	2003-07-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4221 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: indentation	monate	2003-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4155 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: blaster V1	monate	2003-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4059 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIde: externals	monate	2003-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: load/save file encoding support/	monate	2003-05-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: toolbar/autosave	monate	2003-05-07
\| \| \| \| \| \| \| \| \|	Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fichier de pref coq IDE en ASCII (ENFIN)	filliatr	2003-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	monate	2003-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3949 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide : progressbar	monate	2003-04-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3947 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes ↵	monate	2003-03-26
\| \| \| \| \| \|	locaux. Reparation du Undo avec Section et constantes de meme nom. Decoupe tag modifie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: compact delete event-search start	monate	2003-03-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: .coqidepref en bin. Preferences en plus	monate	2003-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug ↵	monate	2003-03-07
\| \| \| \| \| \|	autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: fenetre de cmmandes . undo correct	monate	2003-03-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIde: Install.ide Revert bugfix.	monate	2003-03-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3741 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: partage -debug avec coqtop	monate	2003-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3736 85f007b7-540e-0410-9357-904b9bb8a0f7
*	IDE: maj	monate	2003-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: copy/paste	monate	2003-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3729 85f007b7-540e-0410-9357-904b9bb8a0f7
*	IDE: debug=false	filliatr	2003-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3725 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: preferences support and optimizations	monate	2003-03-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3724 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide updates: copy/paste enhanced. Optimizing coqide on very large inputs. ↵	monate	2003-02-27
\| \| \| \| \| \|	Contextual colorization. Synchronization problems solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3719 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: preliminary support for mnemonics. Edit menu. Context help now works ↵	monate	2003-02-26
\| \| \| \| \| \|	properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3705 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide : aide sur selection ou sur mot	monate	2003-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3700 85f007b7-540e-0410-9357-904b9bb8a0f7
*	aide contextuelle / menus compilation + print + export	filliatr	2003-02-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3698 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: robustesse / multi-buffers / menus / ... (utilisable)	filliatr	2003-02-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3689 85f007b7-540e-0410-9357-904b9bb8a0f7