diff options
Diffstat (limited to 'test-suite/bugs/opened/1596.v')
| -rw-r--r-- | test-suite/bugs/opened/1596.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 0b576db6b3..820022d995 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,7 +2,6 @@ Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. -Unset Standard Proposition Elimination Names. Set Keyed Unification. |