aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-29 15:11:19 +0000
committerGitHub2021-03-29 15:11:19 +0000
commitc6e9b36f2abc7bf434df8e9a6fea48ba9db4efc0 (patch)
tree9fb619b831abe383c45dd9d50067e512d4f65ac2 /doc/sphinx
parent642e8b769b05c7eea685a44aebd2475a928af6b1 (diff)
parentd7ccf45bbb1b73006c5804bcfc18bb3f6f7c90fd (diff)
Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid
Reviewed-by: anton-trunov
Diffstat (limited to 'doc/sphinx')
0 files changed, 0 insertions, 0 deletions