From f42b081b3501ce3655233bb56412f4dc5d2ff7a6 Mon Sep 17 00:00:00 2001
From: Martin Bodin <martin.bodin@inria.fr>
Date: Tue, 17 Nov 2020 16:55:31 +0100
Subject: [PATCH] Spellcheck.

---
 doc/guidelines.md | 2 +-
 util/ssrlia.v     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/guidelines.md b/doc/guidelines.md
index b993796dc..1bf355e76 100644
--- a/doc/guidelines.md
+++ b/doc/guidelines.md
@@ -31,7 +31,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
 ```
 - When commenting, be careful not to leave any misspelled words: Prosa's CI system comprises a spell-checker that will signal errors.
 - When comments have to contain variable names or mathematical notation, use square brackets (e.g. `[job_cost j]`). You can nest square brackets _only if they are balanced_: `[[t1,t2)]` will not work. In this case, use `<<[t1,t2)>>`.
-- The vocabulary of the spell-checker is extended with the words contained in `scripts/wordlist.pws`. Add new words only if strictly necessary.
+- The vocabulary of the spell-checker is extended with the words contained in [`scripts/wordlist.pws`](scripts/wordlist.pws). Add new words only if strictly necessary.
 - Document the sources of lemmas and theorems in the comments. For example, say something like "Theorem XXX in (Foo & Bar, 2007)", and document at the beginning of the file what "(Foo & Bar, 2007)" refers to.
 
 
diff --git a/util/ssrlia.v b/util/ssrlia.v
index 469fed3d8..b6b80218a 100644
--- a/util/ssrlia.v
+++ b/util/ssrlia.v
@@ -25,7 +25,7 @@ Ltac arith_goal_ssrnat2coqnat :=
   end.
 
 (** Solve arithmetic goals.
-  This tactic first rewrites the context to replace ssreflect's operations
+  This tactic first rewrites the context to replace operations from ssreflect
   to the corresponding operations in the Coq library, then calls [lia]. *)
 
 Ltac ssrlia :=
-- 
GitLab