diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 18:50:24 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-05-18 18:50:24 -0400 |
commit | f79e9db4922f649d08153f09526d5c1c60a7e45c (patch) | |
tree | 6c5c370cbf88f91bd019f14d4127fa7a4c707eab | |
parent | 12b121057d03558b9f1eec76f1cc72bc12c9b699 (diff) |
Revert "Fix Qcanon after changes on injection."
This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
-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 e777c74d3..f0edc9f13 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 _ H. + injection H; clear H; intros. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. |