From 0fb8601151a0e316554c95608de2ae4dbdac2ed3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 2 Nov 2009 18:50:33 +0000
Subject: Remove various useless {struct} annotations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/EquivDec.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Classes')

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index bafbac3f1f..0a35ef45e0 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -130,7 +130,7 @@ Require Import List.
 
 Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
   { equiv_dec :=
-    fix aux (x : list A) y { struct x } :=
+    fix aux (x y : list A) :=
     match x, y with
       | nil, nil => in_left
       | cons hd tl, cons hd' tl' =>
-- 
cgit v1.2.3