aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-05 11:53:36 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-05 11:53:44 +0200
commite497afaccc78e92b71e60878d593273dce0036a1 (patch)
tree52ef75f681c8a4c827977e39f5285591b4334331 /plugins
parent87a60c55292e6e9f8dbcfec4d64cb9ae940618f9 (diff)
Better fix of e5c025
Diffstat (limited to 'plugins')
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
1 files changed, 1 insertions, 1 deletions
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.