-
Andrei Paskevich authored
This commit removes all hard-coded "infix ..", "prefix ..", and "mixfix .." from the rest of the code, and handles the symbolic notation entirely inside Ident. It does not change the notation itself.
0fea401c
Prochaines maintenances programmées: mardi 02/04, lundi 06/05, lundi 03/06
Pour plus d'informations: https://doc-si.inria.fr/display/SU/Gitlab
This commit removes all hard-coded "infix ..", "prefix ..", and "mixfix .." from the rest of the code, and handles the symbolic notation entirely inside Ident. It does not change the notation itself.