aboutsummaryrefslogtreecommitdiff
path: root/translate
AgeCommit message (Collapse)Author
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
2003-04-17Ajout "at next level" dans Notationherbelin
Mise en place structure pour définir un objet en même temps que sa notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-11Ajout option 'Local' à Infix et Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3916 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Affichage des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3913 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Affichage des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3896 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Formattage affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3892 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3889 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Bugs synchronisation pour gestion traduction des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3884 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08Ajout option "Local" à "Open Scope"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Aérer les := et : de "assert"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3851 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteherbelin
ne s'insére pour les références dont tous les arguments sont implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3847 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout VernacReserve et suppression des types re-inferablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3807 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-13Ajout réaffichage SubClassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12Ajout Locate Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3757 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05updatedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3665 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-05Ajout du traducteurdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 03:19:05 +0000