summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorMax Schumacher <maximilianbschumacher@gmail.com>2021-03-21 15:22:27 +0100
committerGitHub <noreply@github.com>2021-03-21 15:22:27 +0100
commit67ec5133a24e84c545c920dabab1d235b53523ad (patch)
tree3720f7541ee7fbcb8086f5e71ada8842b7cde5a1
parent5d2d1cf77c8f4e06c08da4657b152a2b2b06504f (diff)
parent160ecc8be8cdb79994a4c150927b2f4b1d164923 (diff)
Merge pull request #4142 from dbenn/patch-3
[coq/en] remove extra "prove" from comment
-rw-r--r--coq.html.markdown2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq.html.markdown b/coq.html.markdown
index 4c1ad690..bbc613ce 100644
--- a/coq.html.markdown
+++ b/coq.html.markdown
@@ -472,7 +472,7 @@ Proof.
intros A B ab. destruct ab as [ a b ]. apply a.
Qed.
-(* We can prove easily prove simple polynomial equalities using the
+(* We can easily prove simple polynomial equalities using the
automated tactic ring. *)
Require Import Ring.