From 46ad1d27adae081e07b9d463fafd88c33dc01bb7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 25 Jun 2006 22:15:32 +0000
Subject: repetition d'hypotheses dans well_founded_induction_type_2

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Wf.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 17f3e5107d..6e07ea43a9 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -146,6 +146,8 @@ Section Well_founded_2.
   Variable R : A * B -> A * B -> Prop.
 
   Variable P : A -> B -> Type. 
+
+  Section Acc_iter_2.
   Variable
     F :
       forall (x:A) (x':B),
@@ -156,6 +158,7 @@ Section Well_founded_2.
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
          Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+  End Acc_iter_2.
 
   Hypothesis Rwf : well_founded R.
 
-- 
cgit v1.2.3