diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-16 16:34:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-16 16:34:17 +0200 |
| commit | 7e69422ea16c9e323d02fdd7c4927750b40bd2cf (patch) | |
| tree | c7422fd92bfd2c9f9e1604419b830e106a8f649d /test-suite/bugs/closed/HoTT_coq_029.v | |
| parent | f1ecf669d82c8b6d05068e12f96f993982ecb533 (diff) | |
Fix spacing in error message.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_029.v')
0 files changed, 0 insertions, 0 deletions