aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Collapse)Author
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Modules obsoletes de ZArith en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4805 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-04Pour eviter des anomalies au lieu d'erreur en mode traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4791 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter queherbelin
les entiers positifs soient parenthésés en tant qu'arguments de fonction; tant pis, il faudra écrire '-(-x)' au lieu de '--x' Ajout CPatNotation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4754 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Affichage des negatifs au niveau de l'application, et des positifs au dessus ↵herbelin
du niveau du moins unaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4744 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout de Print Visibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4712 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de ↵herbelin
SearchNamed dans SearchAbout git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4697 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵herbelin
par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Divers bugs d'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4665 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16nouvelle syntaxe de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16lettac -> setbarras
suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Changement 'as notation' en 'where notation'; protection 'nat_scope'; ↵herbelin
affichage separe des modules importes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4630 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-13Ajout d'une fonction de recherche sur les composantes du nom des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4608 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-11mise a jour nouvelle syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Ajout printers pour constr et constr_pattern (sans traduction)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4569 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10pr_tactic sans traduction; affichage Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4567 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Des abbreviations pour constrintern.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4546 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵herbelin
incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4537 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Debranchement de l'affichage automatique de Proof par le traducteur (trop ↵herbelin
complique de trouver la bonne indentation); affichage en revanche de Proof s'il existait deja git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4536 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02Pas de renommage des noms de sectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4517 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-02as au niveau de appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4516 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-01Implantation de l'option 'format' des Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4509 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Ajout 'Close Scope'.herbelin
Mise en place de la structure pour un modificateur 'format' de Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4502 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Ajout now_showherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4487 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Ajout 'About'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22Système de renommage des noms de tactiques Ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4446 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-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-19parsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 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-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-12Mise en place affichage spécifique pour le scope des typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4361 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; Mise en place affichage ↵herbelin
spécifique pour le scope des types; 'Delimits' -> 'Delimit' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4357 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Passage des projections au niveau 1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Oubli des guillemets dans Commentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4341 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-10Pretty-pretting fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4340 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Traduction des réferences arguments de commandes non primitives; 'Grammar ↵herbelin
tactic' devient 'Tactic Notation' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4335 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-09Ajout If; protection contre clash dans return_typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4330 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 11:38:00 +0000