diff options
| author | herbelin | 2006-01-21 10:18:20 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-21 10:18:20 +0000 |
| commit | a6a6bf8aaf48be6d12d5d08ef42301236f7b38d8 (patch) | |
| tree | 930f8d3bd3631638c3f8ae2d75af48a7b2849bc5 | |
| parent | c6be9348388c413c4bbad9e15506f99e11423a92 (diff) | |
Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7905 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | theories/Init/Wf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 5a05f7b653..3d4d0efbab 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -29,8 +29,8 @@ Section Well_founded. (** The accessibility predicate is defined to be non-informative *) - Inductive Acc (x: A) : Prop := - Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. + Inductive Acc (a: A) : Prop := + Acc_intro : (forall y:A, R y a -> Acc y) -> Acc a. Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. |