If I destruct a thing involving a bool (or remember a bool), the resulting bool will most likely be called b, b0, b1, …; a natural number will be n, …; and so on. Can I access the same name generation mechanism from Ltac? fresh defaults to H no matter what, I can only pass in a name or string (or several) to use in place of H. What if I don’t have any?

The concrete context I currently want that in is writing a remember variant that flips the equality. (Both rewrite and most library theorems expect the equality to have the opposite direction from what remember generates, and I don’t want to deal with using rewrite <- or symmetry in or whatever all. the. time.)

So far I have:

Tactic Notation "remember'" constr(t) "as" ident(x) "eqn" ":" ident(H) :=
(* NB: using "eqn:" instead of "eqn" ":" in the Notation messes up the grammar *)
remember t as x eqn:H; symmetry in H.
Tactic Notation "remember'" constr(t) "as" ident(x) :=
let H := fresh "Heq" x in remember' t as x eqn:H.

Now I’d also like to have a Tactic Notation "remember'" constr(t) := … that makes nice names like remember does, but I don’t know how to access the name generation mechanism. Any pointers?

I wrote this small library of tactics, where there is a tactic autorename h which does more or less what you suggest.

Require Import LibHyps.LibHyps.
Lemma Foo: forall x y , x < y -> y >= x.
Proof.
intros.
autorename H.
(* or equivalently : *)
intros ; { autorename }.
x, y : nat
h_lt_x_y_ : x < y
============================
y >= x