# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1439668742 14400
# Node ID 582bf8d4ce51b6f91bd4e37ba22be93ddcaeedfe
# Parent  8dddcaaeb67a5f2c01e3da498a103546307bbf7c
Fuller English fix

diff -r 8dddcaaeb67a -r 582bf8d4ce51 src/LogicProg.v
--- a/src/LogicProg.v	Sat Aug 15 15:54:11 2015 -0400
+++ b/src/LogicProg.v	Sat Aug 15 15:59:02 2015 -0400
@@ -777,7 +777,7 @@
 
 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.