From fa4d8ca8db3c61b21c822416b4aa226811409df9 Mon Sep 17 00:00:00 2001
From: Ben Sherman <sherm@mit.edu>
Date: Wed, 25 Apr 2018 22:28:22 -0400
Subject: [PATCH] minus notation should be for subtraction, not set minus

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

diff --git a/HoareLogic.v b/HoareLogic.v
index d01b0ed..971b8bd 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -6,6 +6,8 @@
 Require Import Frap.
 
 
+
+
 (** * Syntax and semantics of a simple imperative language *)
 
 (* Here's some appropriate syntax for expressions (side-effect-free) of a simple
@@ -188,7 +190,7 @@ Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
 
 Infix "+" := plus : reset_scope.
-Infix "-" := minus : reset_scope.
+Infix "-" := Init.Nat.sub : reset_scope.
 Infix "*" := mult : reset_scope.
 Infix "=" := eq : reset_scope.
 Infix "<" := lt : reset_scope.
diff --git a/HoareLogic_template.v b/HoareLogic_template.v
index cfc9eff..67ff954 100644
--- a/HoareLogic_template.v
+++ b/HoareLogic_template.v
@@ -164,7 +164,7 @@ Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
 
 Infix "+" := plus : reset_scope.
-Infix "-" := minus : reset_scope.
+Infix "-" := Init.Nat.sub : reset_scope.
 Infix "*" := mult : reset_scope.
 Infix "=" := eq : reset_scope.
 Infix "<" := lt : reset_scope.