diff options
Diffstat (limited to 'test-suite/bugs/closed/3352.v')
| -rw-r--r-- | test-suite/bugs/closed/3352.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index 555accfd5..bf2f7a9d1 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -32,4 +32,4 @@ simpl. Set Printing Universes. exact hprop_Empty. Defined. -End B.
\ No newline at end of file +End B. |