diff --git a/.gitignore b/.gitignore
index d9ca9f4..0bb7d4b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,4 @@ frap.tgz
 Deep.ml*
 Deeper.ml*
 DeeperWithFail.ml*
+*.dir-locals.el
diff --git a/Interpreters.v b/Interpreters.v
index f37e1ff..ee96392 100644
--- a/Interpreters.v
+++ b/Interpreters.v
@@ -346,7 +346,7 @@ Definition factorial_body :=
  * Note that here we're careful to put the quantified variable [input] *first*,
  * because the variables coming after it will need to *change* in the course of
  * the induction.  Try switching the order to see what goes wrong if we put
- * [input] later. *)
+e * [input] later. *)
 Lemma factorial_ok' : forall input output v,
   v $? "input" = Some input
   -> v $? "output" = Some output