-
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: lundi 06/05, lundi 03/06, lundi 01/07
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.