diff --git a/HoareLogic.v b/HoareLogic.v
index 46e6f37..c80246f 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).
@@ -224,9 +215,15 @@ Qed.
  * rules.  Some other obligations are generated, generally of implications
  * between assertions, and [ht] also makes a best effort to solve those. *)
 
-Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
-            || eapply HtIf || eapply HtWhile || eapply HtAssert
-            || eapply HtStrengthenPost.
+Ltac ht1 :=
+  match goal with
+  | [  |- {{ _ }} _ {{ ?P }} ] =>
+    tryif is_evar P then
+      apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
+      || eapply HtIf || eapply HtWhile || eapply HtAssert
+    else
+      eapply HtStrengthenPost
+  end.
 
 Ltac t := cbv beta; propositional; subst;
           repeat match goal with
diff --git a/HoareLogic_template.v b/HoareLogic_template.v
index d64d1b9..b1496ce 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).
@@ -194,9 +186,15 @@ Qed.
  * rules.  Some other obligations are generated, generally of implications
  * between assertions, and [ht] also makes a best effort to solve those. *)
 
-Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
-            || eapply HtIf || eapply HtWhile || eapply HtAssert
-            || eapply HtStrengthenPost.
+Ltac ht1 :=
+  match goal with
+  | [  |- {{ _ }} _ {{ ?P }} ] =>
+    tryif is_evar P then
+      apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
+      || eapply HtIf || eapply HtWhile || eapply HtAssert
+    else
+      eapply HtStrengthenPost
+  end.
 
 Ltac t := cbv beta; propositional; subst;
           repeat match goal with