From 06cd051d140a183229cd43f0bbae152d6ad8d6ca Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sun, 22 Jul 2018 18:19:26 -0400 Subject: Correct some spelling errors Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`. --- test-suite/bugs/closed/bug_4132.v | 2 +- test-suite/success/univers.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v index 806ffb771f..67ecc3087f 100644 --- a/test-suite/bugs/closed/bug_4132.v +++ b/test-suite/bugs/closed/bug_4132.v @@ -26,6 +26,6 @@ Qed. Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. omega. (* Pierre L: according to a comment of bug report #4132, - this might have triggered "Failure(occurence 2)" in the past, + this might have triggered "Failure(occurrence 2)" in the past, but I never managed to reproduce that. *) Qed. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 2863404590..28426b5700 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,7 +60,7 @@ Qed. Record U : Type := { A:=Type; a:A }. -(** Check assignement of sorts to inductives and records. *) +(** Check assignment of sorts to inductives and records. *) Variable sh : list nat. -- cgit v1.2.3