coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	'::' est deja pris en V7	herbelin	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Section et report Infix hors section	herbelin	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le ↵	herbelin	2003-09-19
\| \| \| \| \| \|	traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin	2003-09-19
\| \| \| \| \| \| \|	v8 même si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation :: pour cons	herbelin	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵	herbelin	2003-09-19
\| \| \| \| \| \|	meme si incompatible avec la syntaxe v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4417 85f007b7-540e-0410-9357-904b9bb8a0f7
*	parsing	herbelin	2003-09-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Interface Eauto	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction de Instantiate	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4414 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Niveau du 'as' des motifs	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Traduction de '_' comme reference	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing correct des explicites en cas de projection	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4411 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin	2003-09-18
\| \| \| \| \| \| \|	le fichier chargé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4410 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4409 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplification afficheur de tactiques non primitive	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug fix: term reduced in bad env	barras	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	En attendant l'afficheur...	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4405 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour appliquer les noms reserves aussi aux binders	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour cacher le contenu de Load au traducteur	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4403 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative amelioration pretty-printing symboles	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4402 85f007b7-540e-0410-9357-904b9bb8a0f7
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont ↵	herbelin	2003-09-16
\| \| \| \| \| \|	Record); args scope dans Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4401 85f007b7-540e-0410-9357-904b9bb8a0f7
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reprise de coqbinaries dans translation	herbelin	2003-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4399 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug PR#324	herbelin	2003-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisie	herbelin	2003-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4397 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement de Declare vers Termops	herbelin	2003-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4395 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour à des cibles plus explicites: world7 et world8, install7 et install8	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4394 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Outil de test de la traduction et de la compilation en v8 sans modification des	herbelin	2003-09-12
\| \| \| \| \| \| \|	sources git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4393 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout install7 et coqwc dans tools	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4392 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout cible world7	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4391 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Divers	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4390 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout nouvelles commandes	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4389 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵	herbelin	2003-09-12
\| \| \| \| \| \| \| \| \| \|	choix du parseur en fonction de cette option Suppression DatatypesSyntax et PeanoSyntax qui était vides git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵	herbelin	2003-09-12
\| \| \| \| \| \| \| \| \|	choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression DatatypesSyntax et PeanoSyntax qui était vides	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion des g_syntaxnew.ml avec les g_syntax.ml avec sélection dynamique selon	herbelin	2003-09-12
\| \| \| \| \| \| \|	l'option v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4385 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inclusion automatique de highparsing	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4384 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression DatatypesSyntax et PeanoSyntax qui était vides	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4383 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Message pour les erreurs	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4382 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage au numéro de version V8	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4381 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4380 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4379 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4378 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ module requis pour le parsing des numéraux	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4377 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des scopes d'arguments	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout et MAJ commandes de scopes	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4375 85f007b7-540e-0410-9357-904b9bb8a0f7