Goal:
    H : False
  ============================
   (nth_error ?list_all match H return nat with
                        end = Some H)


DEBUG:Going to execute:
case t

Goals:

DEBUG:Going to execute:
clear t
DEBUG LTAC Evaluated term: H

Goals:

DEBUG:Going to execute:
unshelve
(repeat
  match goal with
  | |- nth_error (?x :: _) 0 = ?rhs => change (Some x = rhs)
  | |- nth_error (_ :: ?xs) (S ?n) = ?rhs => change (nth_error xs n = rhs)
  | |- nth_error ?ev _ = ?rhs =>
        is_evar ev; (let __ := open_constr:((eq_refl : ev = _ :: _)) in
                     idtac)
  | |- Some _ = Some _ => reflexivity
  end)

Goals:

DEBUG:Going to execute:
<coq-core.plugins.ltac::unshelve@0> $1

Goals:

DEBUG:Going to execute:
try exact []