Coq: local ltac definition

Display all goals and responses

Question

If there is a way to define a "local" Ltac expresion which I can use to proof a lemma but not visible outside?

Lemma Foo ...
Proof.
  Ltac ll := ...
  destrict t.
  - reflexivity.
  - ll.
  - ll.
Qed.

(* ll should not be visible here *)

You can use a section:

Section Foo.
  Ltac solve := exact I.
  Lemma Foo : True.True
  Proof.True
    solve.
  Qed.
End Foo.