diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 09:04:29 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-27 09:04:29 +0100 |
commit | 7fa691096df2ab8924f3449f588a6a9d6c81b5f7 (patch) | |
tree | 9c3e027c57f128be8842ede617bb4c847b60495c /theories/NArith/Ndist.v | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
parent | ecebaa47890662c2dcb1e6c146a7299f1ed2b1e3 (diff) |
Merge PR #6473: Fix warning about shadowing a global name.
Diffstat (limited to 'theories/NArith/Ndist.v')
0 files changed, 0 insertions, 0 deletions