diff --git a/src/LogicProg.v b/src/LogicProg.v
index 9be6b6784059010a378c34e9e2132683bc259195..75fda73a950d1dc41a1645d8482a30e2646bb81c 100644
--- a/src/LogicProg.v
+++ b/src/LogicProg.v
@@ -777,7 +777,7 @@ Qed.
 
 Hint Resolve plus_0 times_1.
 
-(** We finish with one more arithmetic lemma that is particularly specialized to this theorem.  This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
+(** We finish with one more arithmetic lemma that is particularly specialized to this theorem.  This fact happens to follow by the axioms of the _semiring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
 
 Require Import Arith Ring.