diff options
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 293a81f14d..0929d965ac 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -202,7 +202,7 @@ Section Zlength_properties. case l; auto. intros x l'; simpl (length (x :: l')) in |- *. rewrite Znat.inj_S. - intros; elimtype False; generalize (Zle_0_nat (length l')); omega. + intros; exfalso; generalize (Zle_0_nat (length l')); omega. Qed. End Zlength_properties. |