From 2ed1d52171bdda1e610184f3a543f0c7333b6280 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= <clement.pitclaudel@live.com>
Date: Mon, 12 Apr 2021 15:04:56 -0400
Subject: [PATCH] =?UTF-8?q?Get=20rid=20of=20the=20=E2=80=9Creset=E2=80=9D?=
 =?UTF-8?q?=20scope=20in=20HoareLogic.v?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It's not needed, and it makes everything harder to read.
---
 HoareLogic.v          | 11 +----------
 HoareLogic_template.v | 10 +---------
 2 files changed, 2 insertions(+), 19 deletions(-)

diff --git a/HoareLogic.v b/HoareLogic.v
index 1ca0273..834cd1c 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -191,20 +191,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
 Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
 Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
-
-(*Declare Scope reset_scope.*)
-Infix "+" := plus : reset_scope.
-Infix "-" := Init.Nat.sub : reset_scope.
-Infix "*" := mult : reset_scope.
-Infix "=" := eq : reset_scope.
-Infix "<" := lt : reset_scope.
-Delimit Scope reset_scope with reset.
-Open Scope reset_scope.
 (* END macros *)
 
 (* We should draw some attention to the next notation, which defines special
  * lambdas for writing assertions. *)
-Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0).
+Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
 
 (* And here's the classic notation for Hoare triples. *)
 Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).
diff --git a/HoareLogic_template.v b/HoareLogic_template.v
index a196e23..5ddce34 100644
--- a/HoareLogic_template.v
+++ b/HoareLogic_template.v
@@ -162,19 +162,11 @@ Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at
 Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
 Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
-
-Infix "+" := plus : reset_scope.
-Infix "-" := Init.Nat.sub : reset_scope.
-Infix "*" := mult : reset_scope.
-Infix "=" := eq : reset_scope.
-Infix "<" := lt : reset_scope.
-Delimit Scope reset_scope with reset.
-Open Scope reset_scope.
 (* END macros *)
 
 (* We should draw some attention to the next notation, which defines special
  * lambdas for writing assertions. *)
-Notation "h & v ~> e" := (fun h v => e%reset) (at level 85, v at level 0).
+Notation "h & v ~> e" := (fun h v => e%nat%type) (at level 85, v at level 0).
 
 (* And here's the classic notation for Hoare triples. *)
 Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next level).