aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Collapse)Author
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
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@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
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
2003-09-03Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Contorsions pour que l'interpretation deses foncteurs depende des parametres ↵herbelin
de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4294 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-02Bug traduction Search, SearchPattern, etc.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4290 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-31Bug et améliorations diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4285 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-14Amélioration affichage syntaxe modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4271 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-13Hack pour ajouter Proof apres Correctnessherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4266 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-12Bug et amliorations diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Ajout systématique de Proof dans la traductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4202 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Formattage Apply withherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4201 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-23Formattage pattern 'match'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4200 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-19Ajout 'Symmetry in Hyp'; chgt syntaxe 'change ... with ...'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4184 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du ↵herbelin
traducteur à proprement parler git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4139 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Ajout notation c.(f) en v8 pour les projections de Record; raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4123 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Raffinement diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4122 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Globalisation des tactiques avant traduction pour capture des noms; ↵herbelin
affinement divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4121 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-24Ajout FreshIdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-22Ajout V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4064 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ↵herbelin
points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Prise en compte notation dans Inductif pour traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4039 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4005 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Separation entre les 2 propositions de syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4004 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07coqide: toolbar/autosavemonate
Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
Suite mise en place infrastructure pour déclaration de syntaxe simultanée à la déclaration d'inductifs Table séparée pour les précédences de notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3983 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et ↵herbelin
n:=c dans les 'with bindings'; mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3975 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
définitions de tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3968 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-27Reparation affichage LetTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3958 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 14:27:05 +0000