aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/_CoqProject
diff options
context:
space:
mode:
authoraffeldt-aist2019-11-14 20:49:44 +0900
committerCyril Cohen2019-12-11 14:26:52 +0100
commitb3261c9020105f3c6667697b22ca8a542271bc4c (patch)
treef7c6918d64decf70ce01d0bf5d21e868532402a8 /mathcomp/_CoqProject
parent050ad8395fb250e9396b7a376a75c523567e177c (diff)
renaming NormedZmoduleType and NormedZmoduleMixin (#416)
* renaming NormedZmoduleType -> NormedZmodType NormedZmoduleMixin -> NormedZmodMixin that looks more homogeneous with regard to naming conventions used so far * update .gitlab-ci.yml * typo
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions