named_goals_interactive_usage.v

Require Import String.
Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).

Tactic Notation "proving" "goal" constr(name) :=
  match goal with
  | |- named_goal _ name => unfold named_goal
  | _ => fail 1 "current goal is not '" name "'"
  end
.

(* example: *)

Goal (nat * nat).
refine ( (_as "a", _as "b") ).
(* proving goal "b"%string.  <-- error *)
proving goal "a"%string.
exact 1.
proving goal "b"%string.
exact 2.
Defined.