aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-18 11:47:11 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-18 11:47:11 +0200
commit0be7f92624494b00cf114914cb04a7443f15746f (patch)
tree6978dbe6d7b251629faf85a81ac984e519386469 /theories/FSets
parentf08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff)
Fix #7829: Spurious documentation failures.
We split a Require Import in two to avoid reaching the timeout.
Diffstat (limited to 'theories/FSets')
0 files changed, 0 insertions, 0 deletions