aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/_CoqProject
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2020-04-21 01:52:32 +0900
committerKazuhiko Sakaguchi2020-04-21 01:52:32 +0900
commitc67dde4080b9c4470b8ab4ff828707fb0044d3dc (patch)
tree2a3aa7215f7bbf8b11ece9c2e794df32dcb9ca36 /mathcomp/_CoqProject
parent709756f9bbb92b5e5844e0133627271c974a11c2 (diff)
Add dual_finLatticeType and fix dual_finDistrLatticeType
This fixes two issues: - dual_finLatticeType was missing, and - dual_finDistrLatticeType was just an identity function.
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions