summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/1596.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/opened/1596.v')
-rw-r--r--test-suite/bugs/opened/1596.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 7c5dc416..820022d9 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.
@@ -258,4 +257,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.