aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate
Commit message (Collapse)AuthorAge
* Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de ↵Gravatar herbelin2003-10-22
| | | | | | SearchNamed dans SearchAbout git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4697 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
| | | | | | | 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
* Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵Gravatar herbelin2003-10-21
| | | | | | par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Divers bugs d'affichageGravatar herbelin2003-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4665 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle syntaxe de ltacGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
* lettac -> setGravatar barras2003-10-16
| | | | | | | 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
* Changement 'as notation' en 'where notation'; protection 'nat_scope'; ↵Gravatar herbelin2003-10-14
| | | | | | affichage separe des modules importes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction de recherche sur les composantes du nom des objetsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4608 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour nouvelle syntaxeGravatar barras2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printers pour constr et constr_pattern (sans traduction)Gravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4569 85f007b7-540e-0410-9357-904b9bb8a0f7
* pr_tactic sans traduction; affichage InversionGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4567 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage en v8 de PolyList en List et List en MonoListGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des abbreviations pour constrintern.mlGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵Gravatar herbelin2003-10-08
| | | | | | incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'Gravatar herbelin2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4537 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debranchement de l'affichage automatique de Proof par le traducteur (trop ↵Gravatar herbelin2003-10-07
| | | | | | 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
* Pas de renommage des noms de sectionGravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4517 85f007b7-540e-0410-9357-904b9bb8a0f7
* as au niveau de appGravatar herbelin2003-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4516 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implantation de l'option 'format' des NotationsGravatar herbelin2003-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4509 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
| | | | | | | 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
* Syntaxe plus liberale pour le type des arguments de filtrage du 'match'Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout now_showGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4487 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'About'Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
* traducteur: affiche les commentaires a l'interieur des commandesGravatar barras2003-09-22
| | | | | | | 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
* Système de renommage des noms de tactiques LtacGravatar herbelin2003-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages divers.Gravatar herbelin2003-09-21
| | | | | | | | | | 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
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
* parsingGravatar herbelin2003-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction de InstantiateGravatar herbelin2003-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Niveau du 'as' des motifsGravatar herbelin2003-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour appliquer les noms reserves aussi aux bindersGravatar herbelin2003-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4404 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place affichage spécifique pour le scope des typesGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Print Scopes' et 'Bind Scope with classes'; Mise en place affichage ↵Gravatar herbelin2003-09-12
| | | | | | 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
* Passage des projections au niveau 1Gravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli des guillemets dans CommentsGravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4341 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty-pretting fixGravatar herbelin2003-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4340 85f007b7-540e-0410-9357-904b9bb8a0f7
* Traduction des réferences arguments de commandes non primitives; 'Grammar ↵Gravatar herbelin2003-09-09
| | | | | | tactic' devient 'Tactic Notation' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout If; protection contre clash dans return_typeGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place possibilité de définitions locales dans les paramètres des ↵Gravatar herbelin2003-09-06
| | | | | | records git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place possibilité de définitions locales dans les paramètres des ↵Gravatar herbelin2003-09-06
| | | | | | inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4319 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place possibilité de définitions locales dans les paramètres des ↵Gravatar herbelin2003-09-06
| | | | | | inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage de lconstr à constr pour les arguments immédiat de commandesGravatar herbelin2003-09-06
| | | | | | | | et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'Gravatar herbelin2003-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contorsions pour que l'interpretation deses foncteurs depende des parametres ↵Gravatar herbelin2003-09-02
| | | | | | de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug traduction Search, SearchPattern, etc.Gravatar herbelin2003-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug et améliorations diversGravatar herbelin2003-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration affichage syntaxe modulesGravatar herbelin2003-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4271 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-16 11:12:02 +0000