REFL_TAC

Tactic.REFL_TAC : tactic

Solves a goal which is an equation between alpha-equivalent terms.

When applied to a goal A ?- t = t', where t and t' are alpha-equivalent, REFL_TAC completely solves it.

    A ?- t = t'
   =============  REFL_TAC

Failure

Fails unless the goal is an equation between alpha-equivalent terms.

See also

Tactic.ACCEPT_TAC, Tactic.MATCH_ACCEPT_TAC, Rewrite.REWRITE_TAC