-
Andrei Paskevich authored
Rename as little as possible and keep the API. Make all the necessary checks in Term and Decl. Remove the duplicate code in Term but keep it elsewhere. We will factorize the code as we go, without rush.
6258e2fd
La mise à jour de gitlab est terminée. Nous sommes désormais en version 16.11.1
Merci de consulter la release note:
https://about.gitlab.com/releases/2024/04/18/gitlab-16-11-released/
Rename as little as possible and keep the API. Make all the necessary checks in Term and Decl. Remove the duplicate code in Term but keep it elsewhere. We will factorize the code as we go, without rush.