From 0ab98d3380033b58162015656f435ae90b936856 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 2 Mar 2017 10:58:28 -0500 Subject: make 8.5 happy --- src/Algebra/Field.v | 2 +- src/Algebra/IntegralDomain.v | 11 +++++------ 2 files changed, 6 insertions(+), 7 deletions(-) (limited to 'src/Algebra') diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index e901bde2f..76b2a9ed3 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -271,7 +271,7 @@ Ltac _inverse_to_equation_by fld d tac := lazymatch goal with | H: eq (mul ?di d) one |- _ => rewrite <-!(left_inv_unique(H:=fld) _ _ H) in * | H: eq (mul d ?di) one |- _ => rewrite <-!(right_inv_unique(H:=fld) _ _ H) in * - | _ => _introduce_inverse constr:(fld) constr:(d) d_nz + | _ => _introduce_inverse fld d d_nz end; clear d_nz. diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 72414b46e..f58874710 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -45,13 +45,12 @@ Module IntegralDomain. | Coef_add c1 c2 => Z.add (CtoZ c1) (CtoZ c2) | Coef_mul c1 c2 => Z.mul (CtoZ c1) (CtoZ c2) end. - Local Notation of_Z := (@Ring.of_Z R zero one opp add). + Let of_Z := (@Ring.of_Z R zero one opp add). Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c. Proof. - Set Printing All. induction c; simpl CtoZ; simpl denote; - repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity. + repeat (rewrite_hyp ?* || Ring.push_homomorphism of_Z); reflexivity. Qed. (* TODO: move *) @@ -77,7 +76,7 @@ Module IntegralDomain. Proof. rewrite <-List.Forall_forall in H; induction H; simpl List.fold_right. { eapply char_ge_C; assumption. } - { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism constr:(of_Z). + { rewrite Znat.N2Z.inj_mul; Ring.push_homomorphism of_Z. eapply Ring.nonzero_product_iff_nonzero_factor; eauto. } Qed. @@ -116,8 +115,8 @@ Module IntegralDomain. | _ => progress (change (denote (Coef_one)) with (of_Z 1) in * ) | _ => progress (change (denote (Coef_opp c)) with (opp (denote c)) in * ) | _ => progress (change (denote (Coef_mul c1 c2)) with (denote c1 * denote c2) in * ) - | |- opp _ <> zero => setoid_rewrite Ring.opp_zero_iff - | |- _ * _ <> zero => eapply Ring.nonzero_product_iff_nonzero_factor + | |- (opp _ <> zero)%type => setoid_rewrite Ring.opp_zero_iff + | |- (mul _ _ <> zero)%type => eapply Ring.nonzero_product_iff_nonzero_factor | _ => solve [eauto using is_constant_nonzero_correct, Pos.le_1_l] | _ => progress rewrite <-CtoZ_correct end. -- cgit v1.2.3