diff --git a/doc/autobound.md b/doc/autobound.md
index 12c97703e5..5586652f70 100644
--- a/doc/autobound.md
+++ b/doc/autobound.md
@@ -5,7 +5,7 @@ However, functions such as `compose` are still quite verbose to define. Note tha
 polymorphic `compose` is even more verbose than the one previously defined.
 
 ```lean
-universes u v w
+universe u v w
 def compose {α : Type u} {β : Type v} {γ : Type w}
             (g : β → γ) (f : α → β) (x : α) : γ :=
   g (f x)
diff --git a/doc/dep.md b/doc/dep.md
index e0d28c9ffe..a8254c1d3f 100644
--- a/doc/dep.md
+++ b/doc/dep.md
@@ -44,7 +44,7 @@ dependent Cartesian product types ``(a : α) × β a`` generalize the Cartesian
 called *sigma* types, and you can also write them as `Σ a : α, β a`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
 
 ```lean
-universes u v
+universe u v
 
 def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
   ⟨a, b⟩
diff --git a/doc/highlight.js b/doc/highlight.js
index 6fba0bf884..ad36345deb 100644
--- a/doc/highlight.js
+++ b/doc/highlight.js
@@ -1111,7 +1111,7 @@ hljs.registerLanguage("lean", function(hljs) {
       'axiom constant ' +
       'partial unsafe private protected ' +
       'if then else ' +
-      'universe universes variable variables ' +
+      'universe variable variables ' +
       'import open export theory prelude renaming hiding exposing ' +
       'calc  match with do by let extends ' +
       'for in unless try catch finally mutual mut return continue break where rec ' +