coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	fin des conclusions multiples	corbinea	2007-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add the possibility to change the position of tabs in main window (from r9717).	glondu	2007-04-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix a bug which sometimes made coqide crash after changing	glondu	2007-04-16
\| \| \| \| \| \| \|	preferences (first fixed in rev. 9716). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau	2007-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 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
*	decl mode: anonymous facts	corbinea	2007-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	addition du neq unicode	letouzey	2007-01-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des modifeurs par défaut dans CoqIDE (problème de ↵	notin	2006-11-07
\| \| \| \| \| \|	compatibilité entre architecture) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit 9256: autres cas incorrects de prise en compte de @ dans les ident	herbelin	2006-10-28
\| \| \| \| \| \| \|	pour F4 dans CoqIDE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9307 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
*	fixed non-bug #1213	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas d'@ dans les identificateurs (pour F4 and co)	herbelin	2006-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9256 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin	2006-10-19
\| \| \| \| \| \| \| \| \|	telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des options Coqide suggérées par Damien Doligez (wish #1053)	notin	2006-10-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9240 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des warnings à la compilation	notin	2006-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Declarative Proof Language: main commit	corbinea	2006-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin	2006-09-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifications dans les scripts de configuration (coqtop et coqide affichent ↵	notin	2006-07-28
\| \| \| \| \| \|	maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement VernacDebug par VernacSetOption (suite)	herbelin	2006-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9024 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin	2006-06-09
\| \| \| \| \| \| \| \|	pour inhiber la gestion de Geoproof sous Coqide (qui peut poser des problèmes avec GTK < 2.6.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #728(1086) (ordre de sauvegarde des tactiques dans coqide)	notin	2006-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8920 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
*	Colorisation dans Coqide	notin	2006-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #990 (LoadPath et option -R de coqide	notin	2006-05-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des warning gtk comme warning coq	herbelin	2006-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8776 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8623@thot: notin \| 2006-03-08 12:40:57 +0100	notin	2006-03-08
\| \| \| \| \| \| \|	Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
\| \| \| \| \| \| \|	et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	barras	2006-01-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7803 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changing the name of drgeocaml into GeoProof	narboux	2005-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide send a ack to tell drgeocaml it is received	narboux	2005-11-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7614 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
*	Détection de la version de lablgtk (type GText.view)	herbelin	2005-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7581 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Détection de la version de lablgtk (type GText.view)	herbelin	2005-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7580 85f007b7-540e-0410-9357-904b9bb8a0f7
*	implement support for drgeocaml	narboux	2005-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7575 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
*	Types inductifs parametriques	mohring	2005-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	improves shadows in the main window	narboux	2005-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7232 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de code commente	coq	2005-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7
*	whelp + correction bug affichage de coqide	coq	2005-06-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Achèvement du déplacement de fonctionnalités unix et browser de ide vers lib	herbelin	2005-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7046 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
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Module/Declare Module syntax made more uniform:	sacerdot	2005-01-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Complétion déclarations coqide	herbelin	2004-11-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7