aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/field
diff options
context:
space:
mode:
authorKazuhiko Sakaguchi2019-04-18 15:06:18 +0200
committerKazuhiko Sakaguchi2019-04-18 16:22:48 +0200
commit10e688f72239e75fbe8d8ea0c84c468569f49a96 (patch)
tree02949d8d9f505274784b834ecb1f89844b035598 /mathcomp/field
parent4e33a068c5451a37d36d94714c966232bc130626 (diff)
Remove unused `Require`s and a hint directive from interval.v
Diffstat (limited to 'mathcomp/field')
0 files changed, 0 insertions, 0 deletions