When applied to a goal A ?- !p. t, the tactic PGEN_TAC reduces it to
A ?- t[p'/p] where p' is a variant of the paired variable structure p
chosen to avoid clashing with any variables free in the goal’s assumption list.
Normally p' is just p.
A ?- !p. t
============== PGEN_TAC
A ?- t[p'/p]