diff options
Diffstat (limited to 'test-suite/bugs/opened/1596.v')
| -rw-r--r-- | test-suite/bugs/opened/1596.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 7c5dc4167..0b576db6b 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -258,4 +258,4 @@ n). apply SynInc;apply H.mem_2;trivial. rewrite H in H0. discriminate. (* !! impossible here !! *) Qed. -End B.
\ No newline at end of file +End B. |