aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/NArith/Ndist.v
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-22 16:01:25 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-22 16:01:25 +0100
commitdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (patch)
treef54c7bffd448f39538187aefedd641698805153f /theories/NArith/Ndist.v
parentff5d440a8158c1ae46604c9557b495e3f45eb077 (diff)
parentce22501ca90e3c6e7124de4eeb4ad3c0a2615666 (diff)
Merge PR #6465: Gitlab touchup
Diffstat (limited to 'theories/NArith/Ndist.v')
0 files changed, 0 insertions, 0 deletions