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/Program/Wf.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 9b7ea04748..c4d06fd722 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -27,7 +27,7 @@ Section Well_founded.
 
   Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
 
-  Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
+  Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x :=
     F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y)
       (Acc_inv r (proj2_sig y))).
 
-- 
cgit v1.2.3