diff options
Diffstat (limited to 'theories/QArith/Qcanon.v')
| -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 05a27cc43..c20c3ba7f 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -488,7 +488,7 @@ Definition Qc_eq_bool (x y : Qc) := Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. Proof. - intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. + intros x y; unfold Qc_eq_bool; case (Qc_eq_dec x y); simpl; auto. intros _ H; inversion H. Qed. |