From 6c1d09bbbcd5aff735760396ba5da1b82be8776f Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 29 Jan 2022 16:28:31 -0500
Subject: [PATCH] Revising for next lecture

---
 BasicSyntax.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/BasicSyntax.v b/BasicSyntax.v
index 1c56c5c..747dd86 100644
--- a/BasicSyntax.v
+++ b/BasicSyntax.v
@@ -206,7 +206,7 @@ Module ArithWithVariables.
    * We use an infix operator [==v] for equality tests on strings.
    * It has a somewhat funny and very expressive type,
    * whose details we will try to gloss over.
-   * (To dig into it more on your own, the appropriate keyword is "dependent types.") *)
+   * (We later return to them in SubsetTypes.v.) *)
   Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
     match inThis with
     | Const _ => inThis
@@ -469,7 +469,7 @@ Module ArithWithVariables.
     linear_arithmetic.
   Qed.
 
-  Hint Rewrite n_times_0.
+  Local Hint Rewrite n_times_0.
   (* Registering rewrite hints will get [simplify] to apply them for us
    * automatically! *)