Display shelved goals without BehindModal

diaframe/steps/small_steps.v

@@ -81,7 +81,7 @@ Ltac trySolvePurePreSplit Δφ R :=
     (* somehow prepending idtac changes the semantics and makes it work like intentioned...?*)
     (idtac; fail 1 "Pure condition"φ"needs to be proved now!"))
   (* final option: solve it now, and if unsuccesful, shelve it *)
-   | split; [first [solve [maybeIPureIntro; trySolvePure] | shelve] | ] ].
+   | split; [first [solve [maybeIPureIntro; trySolvePure] | (change φ with φr; shelve)] | ] ].
 
 Ltac introStepNT namer_tac := (* used for iReIntro tactic *)
   (simplify_eq; subst) ||