aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2014-03-12 10:46:49 -0400
committerGravatar Maxime Dénès <mail@maximedenes.fr>2014-07-22 17:52:08 -0400
commite0c70fc7cd8333a48a4bac47bcb0e01e4b737718 (patch)
tree54419590bb77ed885e50cee0f2955dddeb7ba4fa /theories/Vectors
parent9c9f5a3bde48a46c8e5146093392883ee16bc9e2 (diff)
Fixed proof of irrelevance of le on nat, inspired by the
corresponding proof in ssreflect.
Diffstat (limited to 'theories/Vectors')
0 files changed, 0 insertions, 0 deletions