diff options
Diffstat (limited to 'theories/Sets/Relations_3.v')
| -rwxr-xr-x | theories/Sets/Relations_3.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index d6202cffe..ec8fb7e6d 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -46,9 +46,9 @@ Section Relations_3. Definition Confluent : Prop := forall x:U, confluent x. - Inductive noetherian : U -> Prop := + Inductive noetherian (x: U) : Prop := definition_of_noetherian : - forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x. + (forall y:U, R x y -> noetherian y) -> noetherian x. Definition Noetherian : Prop := forall x:U, noetherian x. |