diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-30 01:12:44 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-30 01:12:44 -0400 |
| commit | f3b3b6e4d01080da4f0ce37a06553769e9588d0e (patch) | |
| tree | 8566d16013d5f98d43e8a3843e9cf75040aa5503 /theories/QArith | |
| parent | 3092819d4e3e1d0995c8156be0b98dce0afbcb9a (diff) | |
Fix Qcanon after changes on injection.
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qcanon.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 1826b607d..e395e4d03 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -254,7 +254,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H; clear H; intros. + injection H; clear H; intros _ H. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. |