diff --git a/theories/biabd/instances_base.v b/theories/biabd/instances_base.v
index fe135b846d7d7c316eaf1d7d3ad2594d8ac2842a..04144ae664325dcec7ac16aca383bcfa60164569 100644
--- a/theories/biabd/instances_base.v
+++ b/theories/biabd/instances_base.v
@@ -87,7 +87,8 @@ Section abduction_instances.
     BiAbd (TTl := TTl) (TTr := TTr) p P Q M R S →
     ModalityMono M →
     (∀.. (ttr : TTr), TCOr (∀.. ttl : TTl, Affine (tele_app (tele_app S ttl) ttr)) (Absorbing (tele_app Q ttr))) →
-    Abduct (TT := TTr) p P Q M (∃.. ttl, tele_app R ttl)%I.
+    Abduct (TT := TTr) p P Q M (∃.. ttl, tele_app R ttl)%I. 
+    (* priority of this instance has a significant performance impact! I think low = better *)
   Proof.
     rewrite /BiAbd /Abduct => /tforall_forall HPR HM /tforall_forall Hdrop.
     apply wand_elim_r', bi_texist_elim => ttl.
diff --git a/theories/heap_lang/class_instances_heaplang.v b/theories/heap_lang/class_instances_heaplang.v
index 426a6f25f847103a082fe8e5aa9ceef5818070d4..ca22a924c090f8b9892901a4abd6dd63b91a17f6 100644
--- a/theories/heap_lang/class_instances_heaplang.v
+++ b/theories/heap_lang/class_instances_heaplang.v
@@ -225,16 +225,10 @@ Ltac find_reshape e K e' TC :=
 Global Hint Extern 4 (ReshapeExprAnd expr ?e ?K ?e' ?TC) => 
   find_reshape e K e' TC : typeclass_instances.
 
-Global Hint Extern 4 (ReshapeExprAnd (language.expr heap_lang) ?e ?K ?e' ?TC) =>
-  find_reshape e K e' TC : typeclass_instances.
-
 Global Hint Extern 4 (ReshapeExprAnd (language.expr ?L) ?e ?K ?e' ?TC) =>
   unify L heap_lang;
   find_reshape e K e' TC : typeclass_instances.
 
-Global Hint Extern 4 (ReshapeExprAnd (language.expr (ectxi_lang heap_ectxi_lang)) ?e ?K ?e' ?TC) =>
-  find_reshape e K e' TC : typeclass_instances.
-
 
 From iris.heap_lang.lib Require Import par.
 
diff --git a/theories/steps/tactics.v b/theories/steps/tactics.v
index e9f67b12570796ef415645dbdd6c02a824c57599..b1ec0e1105ca790108c3895763b6f8cfce1afd26 100644
--- a/theories/steps/tactics.v
+++ b/theories/steps/tactics.v
@@ -9,15 +9,14 @@ Export solve_defs.
 
 Set Universe Polymorphism.
 
-Class AsSolveGoal {PROP : bi} (φ : Prop) (Pin Pout : PROP) :=
-  into_solve_sep : φ → Pout ⊢ Pin.
+Class AsSolveGoal {PROP : bi} (Pin Pout : PROP) :=
+  into_solve_sep : Pout ⊢ Pin.
 
-Lemma from_as_solve_goal {PROP : bi} Δ (P : PROP) P' φ :
-  AsSolveGoal φ P P' →
-  φ →
+Lemma from_as_solve_goal {PROP : bi} Δ (P : PROP) P' :
+  AsSolveGoal P P' →
   envs_entails Δ $ P' →
   envs_entails Δ P.
-Proof. by rewrite envs_entails_eq => HPP /HPP ->. Qed.
+Proof. by rewrite envs_entails_eq => HPP ->. Qed.
 
 Class FromTExistAlways {PROP : bi} (P : PROP) (TT : tele) (P' : TT -t> PROP) :=
   from_texist_always : (∃.. tt, tele_app P' tt) ⊢ P.
@@ -28,6 +27,8 @@ Class CollectModal {PROP : bi} (P : PROP) (M : PROP → PROP) (P' : PROP) :=
 Section coq_tactics.
   Context {PROP : bi}.
   Implicit Types (M : PROP → PROP).
+  (* TODO: alot of AsSolveGoal instances successfully find CollectModal instances before failing later.
+      this can probably be improved *)
 
   Global Instance fromtexist_always_fromtexist (P : PROP) TT P' :
     FromTExist P TT P' →
@@ -42,9 +43,9 @@ Section coq_tactics.
     CollectModal P M P' →
     ModalityMono M →
     FromTExistAlways P' TT P'' →
-    AsSolveGoal True P (SolveOne M P'') | 99.
+    AsSolveGoal P (SolveOne M P'') | 99.
   Proof.
-    rewrite /CollectModal /AsSolveGoal /FromTExistAlways /SolveOne => <- HM HP' _.
+    rewrite /CollectModal /AsSolveGoal /FromTExistAlways /SolveOne => <- HM HP'.
     apply HM => {HM}.
     by rewrite -HP'.
   Qed.
@@ -56,7 +57,7 @@ Section coq_tactics.
     IntroducableModality M →
     FromLaterNMax P' n P'' →
     FromWand P'' H G →
-    AsSolveGoal True P (MergeMod (bi_laterN n) $ IntroduceHyp H G) | 39. (* FromWand does not look under laters, FromForall does... *)
+    AsSolveGoal P (MergeMod (bi_laterN n) $ IntroduceHyp H G) | 39. (* FromWand does not look under laters, FromForall does... *)
   Proof. 
     rewrite /CollectModal /AsSolveGoal /FromLaterNMax /FromWand /MergeMod /IntroduceHyp /= /ModWeaker.
     move => <- <- /= <- <- //.
@@ -67,7 +68,7 @@ Section coq_tactics.
     IntroducableModality M →
     FromLaterNMax P' n P'' →
     FromForall P'' Φ ident →
-    AsSolveGoal True P (MergeMod (bi_laterN n) $ IntroduceVars (TT := [tele_pair A]) Φ) | 50.
+    AsSolveGoal P (MergeMod (bi_laterN n) $ IntroduceVars (TT := [tele_pair A]) Φ) | 50.
   Proof. 
     rewrite /CollectModal /AsSolveGoal /FromLaterNMax /FromForall /MergeMod /IntroduceVars /= /ModWeaker.
     move => <- <- /= <- <- //.
@@ -77,7 +78,7 @@ Section coq_tactics.
     CollectModal P M P' →
     IntroducableModality M →
     FromWand P' H G →
-    AsSolveGoal True P (IntroduceHyp H G) | 38.
+    AsSolveGoal P (IntroduceHyp H G) | 38.
   Proof. 
     rewrite /CollectModal /AsSolveGoal /FromWand /MergeMod /IntroduceHyp /= /ModWeaker /ModalityMono.
     move => <- <- /= -> //.
@@ -87,38 +88,38 @@ Section coq_tactics.
     CollectModal P M P' →
     IntroducableModality M → 
     FromForall P' Φ ident →
-    AsSolveGoal True P (IntroduceVars (TT := [tele_pair A]) Φ) | 40.
+    AsSolveGoal P (IntroduceVars (TT := [tele_pair A]) Φ) | 40.
   Proof. 
     rewrite /CollectModal /AsSolveGoal /FromForall /MergeMod /IntroduceVars /= /ModWeaker.
     move => <- /= <- -> //.
   Qed.
 
   Global Instance later_as_solve_goal (P : PROP) :
-    AsSolveGoal True (â–· P)%I (MergeMod (bi_later) P).
+    AsSolveGoal (â–· P)%I (MergeMod (bi_later) P).
   Proof. rewrite /AsSolveGoal /MergeMod //. Qed.
 
   Global Instance laterN_as_solve_goal (P : PROP) n :
-    AsSolveGoal True (â–·^n P)%I (MergeMod (bi_laterN n) P).
+    AsSolveGoal (â–·^n P)%I (MergeMod (bi_laterN n) P).
   Proof. rewrite /AsSolveGoal /MergeMod //. Qed.
 
   Global Instance solve_sep_as_solve_goal {TT} M P R :
-    AsSolveGoal True (SolveSep (TT := TT) M P R) (SolveSep (TT := TT) M P R) | 20.
+    AsSolveGoal (SolveSep (TT := TT) M P R) (SolveSep (TT := TT) M P R) | 20.
   Proof. rewrite /AsSolveGoal //. Qed.
 
   Global Instance solve_one_as_solve_goal {TT} M P :
-    AsSolveGoal True (SolveOne (TT := TT) M P) (SolveOne (TT := TT) M P) | 20.
+    AsSolveGoal (SolveOne (TT := TT) M P) (SolveOne (TT := TT) M P) | 20.
   Proof. rewrite /AsSolveGoal //. Qed.
 
   Global Instance intuitionistically_as_solve_goal (P : PROP) :
-    AsSolveGoal True (â–¡ P)%I (MergeMod (bi_intuitionistically) P).
+    AsSolveGoal (â–¡ P)%I (MergeMod (bi_intuitionistically) P).
   Proof. rewrite /AsSolveGoal /MergeMod //. Qed.
 
   Global Instance intuitionistically_as_solve_goal_fupd `{BiFUpd PROP} (P : PROP) E :
-    AsSolveGoal True (|={E}=> â–¡ P)%I (MergeMod (bi_intuitionistically) P).
+    AsSolveGoal (|={E}=> â–¡ P)%I (MergeMod (bi_intuitionistically) P).
   Proof. rewrite /AsSolveGoal /MergeMod //. eauto. Qed.
 
   Global Instance make_laterable_as_solve_goal (P : PROP) :
-    AsSolveGoal True (make_laterable P)%I (MergeMod (make_laterable) P).
+    AsSolveGoal (make_laterable P)%I (MergeMod (make_laterable) P).
   Proof. rewrite /AsSolveGoal /MergeMod //. Qed.
 
   Lemma as_emp_valid_weak (φ : Prop) (P : PROP) `{!AsEmpValidWeak φ P} :
@@ -134,9 +135,8 @@ Ltac iStartProof2 :=
   | (notypeclasses refine (as_emp_valid_weak _ _ _); [iSolveTC || fail "iStartProof2: not a BI assertion" | iStartProof]) ].
 
 Ltac iStepS_internal cont :=
-  notypeclasses refine (from_as_solve_goal _ _ _ _ _ _ _);
+  notypeclasses refine (from_as_solve_goal _ _ _ _ _);
     [iSolveTC
-    |try (by auto)
     |simpl; cont].
 
 Ltac iStepS :=