diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 0708e060a..bc3600f9c 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -396,7 +396,7 @@ Variable A : NZ -> Prop. Hypothesis A_wd : predicate_wd NZeq A. Add Morphism A with signature NZeq ==> iff as A_morph. -Proof A_wd. +Proof. apply A_wd. Qed. Section Center. |