aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-08 14:19:29 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-08 14:19:34 +0200
commit7e00e8d602e67810700a7071c419ffd7ef8806c5 (patch)
tree0541e014fc1bf128bb13a816c31d1d4ceb18f51c /theories/Vectors
parent11fc2695936c4cff0eea18cb97f6c83eb7cff09d (diff)
Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits
ago) which broke compilation of theories/Logic/WKL.v (collision between a temporary name and a user name).
Diffstat (limited to 'theories/Vectors')
0 files changed, 0 insertions, 0 deletions