(Est) Minor renaming/restructuring/cleanup

This commit is contained in:
Inari Listenmaa
2022-07-01 08:35:37 +02:00
parent e4a195a777
commit 1b5840c89d
3 changed files with 23 additions and 14 deletions
+1
View File
@@ -56,6 +56,7 @@ concrete ExtendEst of Extend =
linref
VPS = X.linVPS (agrP3 Sg) ;
VPI = X.linVPI InfMa ;
lin
MkVPS = X.MkVPS ;