From e497afaccc78e92b71e60878d593273dce0036a1 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Tue, 5 Aug 2014 11:53:36 +0200 Subject: Better fix of e5c025 --- plugins/setoid_ring/Ring_polynom.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring/Ring_polynom.v') diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 9e88b6c90..5ec73950b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1397,7 +1397,7 @@ Qed. match p with | xI _ => rpow r (Cp_phi (Npos p)) | xO _ => rpow r (Cp_phi (Npos p)) - | 1%positive => r + | 1 => r end == pow_pos rmul r p. Proof. destruct p; now rewrite ?pow_th.(rpow_pow_N). Qed. -- cgit v1.2.3