diff options
| -rw-r--r-- | coq.html.markdown | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq.html.markdown b/coq.html.markdown index b3cc27fc..3a924a19 100644 --- a/coq.html.markdown +++ b/coq.html.markdown @@ -370,7 +370,7 @@ Close Scope string_scope. power series and results,...) • Relations : Relations (definitions and basic results) • Sorting : Sorted list (basic definitions and heapsort correctness) -• Strings : 8-bits characters and strings +• Strings : 8-bit characters and strings • Wellfounded : Well-founded relations (basic results) *) @@ -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. |