From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/opened/1596.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'test-suite/bugs/opened/1596.v') 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. -- cgit v1.2.3