From 5ca744aef261972e3f0c6bbed1ef5bfe1c8cff2e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 May 2014 15:44:27 +0200
Subject: Fixing test-suite for bug #3043.

---
 test-suite/bugs/closed/3043.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/3043.v b/test-suite/bugs/closed/3043.v
index 1be5056f94..654663b4fc 100644
--- a/test-suite/bugs/closed/3043.v
+++ b/test-suite/bugs/closed/3043.v
@@ -1,4 +1,4 @@
-Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = 
+Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig (sig_of_sigT X)) =
      (fun A (P : A -> Prop) (X : sigT P) => projT1 X).
   reflexivity.
 Qed.
-- 
cgit v1.2.3