From 834c6633a37742d0c1be4bd6d270b8e97f9d1348 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 4 Dec 2014 15:58:52 +0100
Subject: Take benefit of improved name preservation of evars in e2fa65fcc.

---
 test-suite/success/destruct.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index d3aca59a2a..83a33f75dc 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -110,7 +110,7 @@ Abort.
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
 do 2 eexists.
 destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
-change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n0).
+change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
 Abort.
 
 (* An example with incompatible but convertible occurrences *)
-- 
cgit v1.2.3