aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate/ppvernacnew.ml
Commit message (Expand)AuthorAge
* Separation entre les propositions de syntaxe - suiteGravatar herbelin2003-05-13
* Separation entre les 2 propositions de syntaxeGravatar herbelin2003-05-13
* coqide: toolbar/autosaveGravatar monate2003-05-07
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Affichage des inductifsGravatar herbelin2003-04-10
* Affichage des inductifsGravatar herbelin2003-04-09
* Formattage affichageGravatar herbelin2003-04-09
* Mécanisme plus simple et efficace pour traduire les implicitesGravatar herbelin2003-04-09
* Bugs synchronisation pour gestion traduction des implicitesGravatar herbelin2003-04-09
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun impliciteGravatar herbelin2003-04-07
* Ajout VernacReserve et suppression des types re-inferablesGravatar herbelin2003-03-31
* *** empty log message ***Gravatar barras2003-03-21
* Ajout réaffichage SubClassGravatar herbelin2003-03-13
* *** empty log message ***Gravatar barras2003-03-12
* Ajout Locate NotationGravatar herbelin2003-03-12
* Ajout du traducteurGravatar desmettr2003-02-05