closer, but

src/tactic/back.lean

@@ -263,7 +263,7 @@ do --trace $ "attempting to apply " ++ to_string e.lem,
          t ← infer_type g,
          relevant_facts ← filter_lemmas t s.facts,
          return { apply_state . goal := g, goal_type := t, committed := e.finishing ∨ committed, step := apply_step.facts, lemmas := relevant_facts }),
-   return ({ goals := as, num_mvars := num_mvars, ..s' }, ff)
+   return ({ goals := as ++ s.goals, num_mvars := num_mvars, ..s' }, ff)
 
 meta def back_state.add_goal (s : back_state) (as : apply_state) :=
 { goals := as :: s.goals .. s }

test/back.lean

@@ -32,7 +32,7 @@ by back?
 example (f : ℕ → ℕ) (x y : ℕ) (p : x = y) : f x = f y :=
 begin
   success_if_fail { back [-congr_arg] },
-  back,
+  back?,
 end
 
 section primes
@@ -56,7 +56,7 @@ begin
     simp at a,
     -- We can restrict the search depth:
     have h₁ : p ∣ M, { back 2 },
-    have h₂ : p ∣ fact N, { back [le_of_lt, prime.pos], },
+    have h₂ : p ∣ fact N, { back? [le_of_lt, prime.pos], },
     have h : p ∣ 1, { back [nat.dvd_add_iff_right] },
     back [prime.not_dvd_one],
   },