From ff206b52832515874f19326b0a12f8d507df2bea Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 15 Aug 2015 15:54:11 -0400
Subject: [PATCH] Two English errors fixed
---
src/LogicProg.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/LogicProg.v b/src/LogicProg.v
index 4d5f421..9be6b67 100644
--- a/src/LogicProg.v
+++ b/src/LogicProg.v
@@ -398,7 +398,7 @@ End slow.
Hint Resolve eq_trans : slow.
(* end thide *)
-Example three_minus_four_zero : exists x, 1 + x = 0.
+Example from_one_to_zero : exists x, 1 + x = 0.
(* begin thide *)
Time eauto.
(** %\vspace{-.15in}%
@@ -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 ring, 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 _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
Require Import Arith Ring.
--
2.18.1