aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rsigma.v
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-10 14:53:18 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-10 14:53:18 +0200
commit38d4b5cba84a253f2f4ea4febda9f60fde2052c9 (patch)
tree1b36a8119643c060e18377e703f687a3cf6ac091 /theories/Reals/Rsigma.v
parenta68c539b6cbe119290df0c6c065cab8ee4746c09 (diff)
parentdda46c6024f8d315111f60393417bbee4db5693e (diff)
Merge PR #7899: My recent improvements to the backport script.
Diffstat (limited to 'theories/Reals/Rsigma.v')
0 files changed, 0 insertions, 0 deletions