diff options
Diffstat (limited to 'test-suite/bugs/closed/348.v')
| -rw-r--r-- | test-suite/bugs/closed/348.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/348.v index 28cc5cb1e..48f0b5512 100644 --- a/test-suite/bugs/closed/348.v +++ b/test-suite/bugs/closed/348.v @@ -9,5 +9,5 @@ End D. Module D' (M:S). Import M. - Definition empty:Set. exact nat. Save. + Definition empty:Set. exact nat. Qed. End D'. |