From 796fc8d64c7b63253acd5040353fbbcb5c42f32d Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Mon, 12 Apr 2021 16:03:38 -0400
Subject: [PATCH] Noticed one invariant in HoareLogic was more complex than
 required

---
 DependentInductiveTypes_template.v | 4 ++--
 HoareLogic.v                       | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/DependentInductiveTypes_template.v b/DependentInductiveTypes_template.v
index 8c41e9b..6303133 100644
--- a/DependentInductiveTypes_template.v
+++ b/DependentInductiveTypes_template.v
@@ -540,7 +540,7 @@ Proof.
   induct s1; simplify; subst; simplify; auto.
 Qed.
 
-Local Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
+Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
 
 (* BOREDOM'S END! *)
 
@@ -635,7 +635,7 @@ Proof.
   induct s; substring.
 Qed.
 
-Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
+Local Hint Extern 1 (String _ _ = String _ _) => f_equal : core.
 
 Lemma substring_stack : forall s n2 m1 m2,
   m1 <= m2
diff --git a/HoareLogic.v b/HoareLogic.v
index c80246f..41863a2 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -398,8 +398,7 @@ Local Hint Extern 1 (_ <= _) => linear_arithmetic : core.
 Theorem selectionSort_ok :
   {{_&_ ~> True}}
     "i" <- 0;;
-    {{h&v ~> v $! "i" <= v $! "n"
-        /\ (forall i j, i < j < v $! "i" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j))
+    {{h&v ~> (forall i j, i < j < v $! "i" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j))
         /\ (forall i j, i < v $! "i" -> v $! "i" <= j < v $! "n" -> h $! (v $! "a" + i) <= h $! (v $! "a" + j)) }}
     while "i" < "n" loop
       "j" <- "i"+1;;