aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/InitialRing.v
diff options
context:
space:
mode:
authorGuillaume Melquiond2014-10-27 07:21:09 +0100
committerGuillaume Melquiond2014-10-27 07:21:09 +0100
commit65c8d91cd4c11b8de44f0b23cd44a3303cd54d4e (patch)
tree5b7c97dc58c1b453cd4ba0df838e5cd7a452e309 /plugins/setoid_ring/InitialRing.v
parentcc81b38185b6f558a6908f64cfaa7ee94131bf6c (diff)
Fix some typos in comments.
Diffstat (limited to 'plugins/setoid_ring/InitialRing.v')
-rw-r--r--plugins/setoid_ring/InitialRing.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 07f49cc4ff..9010917fec 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -815,7 +815,7 @@ Ltac ring_elements set ext rspec pspec sspec dspec rk :=
fun f => f arth ext_r morph lemma1 lemma2
| _ => fail 4 "ring: bad sign specification"
end
- | _ => fail 3 "ring: bad coefficiant division specification"
+ | _ => fail 3 "ring: bad coefficient division specification"
end
| _ => fail 2 "ring: bad power specification"
end