diff --git a/HoareLogic.v b/HoareLogic.v
index 834cd1c..244955d 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -215,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 5ddce34..baae6e2 100644
--- a/HoareLogic_template.v
+++ b/HoareLogic_template.v
@@ -186,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