diff --git a/extras/latex/lstlean.tex b/extras/latex/lstlean.tex
index 2ac9499af7..7453ff9881 100644
--- a/extras/latex/lstlean.tex
+++ b/extras/latex/lstlean.tex
@@ -50,11 +50,11 @@ otherkeywords={
 [persistent], [notation], [visible], [instance], [trans_instance],
 [class], [parsing-only], [coercion], [unfold_full], [constructor], 
 [reducible], [irreducible], [semireducible], [quasireducible], [wf],
-[whnf], [multiple_instances], [none], [decls], [declarations], 
-[coercions], [classes], [symm], [subst], [refl], [trans], [simp], [simps], [congr], 
-[forward], [no_pattern], [notations], [abbreviations], [begin_end_hints], [tactic_hints],
-[reduce_hints], [unfold_hints], [aliases], [eqv], [intro], [intro!], [elim], 
-[localrefinfo] [recursor]
+[whnf], [multiple_instances], [none], [decl], [declaration], 
+[relation], [symm], [subst], [refl], [trans], [simp], [congr], 
+[backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation],
+[reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder],
+[localrefinfo], [recursor]
 },
 
 % Various symbols