aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-09-21Renommage Implicits -> Implicitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4436 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
Nouvelle list de renommage d'idents de v7 en v8 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4435 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Renommages divers.herbelin
Changement de la politique de V8only: V8only tout seul signifie 'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4434 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Parsing au niveau lconstr des patterns de 'match context'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4432 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel). Restructuration de Metasyntax. Correction bug qui cassait l'affichage de la version -translate quand utilisée en v7 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4431 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Mise en place d'implicites par noms en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4429 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵herbelin
aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4428 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant ↵herbelin
aussi à nat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4427 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4426 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19coqide auto complete initial bug fixmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4425 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Coqide : les nouveaute d'aoutmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19'::' est deja pris en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4423 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4422 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Section et report Infix hors sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4421 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le ↵herbelin
traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4420 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Mise en place des V8Notation et V8Infix pour déclarer des notations enherbelin
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
2003-09-19Ajout notation :: pour consherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4418 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 ↵herbelin
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
2003-09-19parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Interface Eautoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4415 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Traduction de Instantiateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4414 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Niveau du 'as' des motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4413 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Traduction de '_' comme referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4412 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Parsing correct des explicites en cas de projectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4411 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Plutôt que de faire "Load" silencieusement, en profiter pour traduireherbelin
le fichier chargé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4410 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4409 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18bug fix: term reduced in bad envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4406 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16En attendant l'afficheur...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4405 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16Pour appliquer les noms reserves aussi aux bindersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4404 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16Pour cacher le contenu de Load au traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4403 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16Tentative amelioration pretty-printing symbolesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4402 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont ↵herbelin
Record); args scope dans Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4401 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-16(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4400 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-15Reprise de coqbinaries dans translationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4399 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-14Bug PR#324herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4398 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-13Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4397 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-13Deplacement de Declare vers Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4395 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Retour à des cibles plus explicites: world7 et world8, install7 et install8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4394 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Outil de test de la traduction et de la compilation en v8 sans modification desherbelin
sources git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4393 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout install7 et coqwc dans toolsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4392 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout cible world7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4391 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4390 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout nouvelles commandesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4389 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
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
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 08:02:09 +0000