Quelle  print_ltac.v   Sprache: Coq

(* Testing of various things about Print Ltac *)
(* https://github.com/coq/coq/issues/10971 *)
Ltac t1 := time "my tactic" idtac.
Print Ltac t1.
Ltac t2 := let x := string:("my tactic") in idtac x.
Print Ltac t2.
Tactic Notation "idtacstr" string(str) := idtac str.
Ltac t3 := idtacstr "my tactic".
Print Ltac t3.
(* https://github.com/coq/coq/issues/9716 *)
Ltac t4 x := match x with ?A => constr:((A, A)) end.
Print Ltac t4.

Notation idnat := (@id nat).
Notation idn := id.
Notation idan := (@id).
Fail Strategy transparent [idnat].
Strategy transparent [idn].
Strategy transparent [idan].
Ltac withstrategy l x :=
  let idx := smart_global:(id) in
  let tl := strategy_level:(transparent) in
  with_strategy 1 [id id] (
  with_strategy l [id id] (
  with_strategy tl [id id] (
  with_strategy 0 [id id] (
  with_strategy transparent [id id] (
  with_strategy opaque [id id] (
  with_strategy expand [id id] (
  with_strategy 0 [idx] (
  with_strategy 0 [id x] (
  with_strategy 0 [x id] (
  with_strategy 0 [idn] (
  with_strategy 0 [idn x] (
  with_strategy 0 [idn id] (
  with_strategy 0 [idn id x] (
  with_strategy 0 [idan] (
  with_strategy 0 [idan x] (
  with_strategy 0 [idan id] (
  with_strategy 0 [idan id x] (
  idtac
    )))))))))))))))))).
Print Ltac withstrategy.

Module Type Empty. End Empty.
Module E. End E.
Module F (E : Empty).
  Definition id {T} := @id T.
  Notation idnat := (@id nat).
  Notation idn := id.
  Notation idan := (@id).
  Fail Strategy transparent [idnat].
  Strategy transparent [idn].
  Strategy transparent [idan].
  Ltac withstrategy l x :=
    let idx := smart_global:(id) in
    let tl := strategy_level:(transparent) in
    with_strategy 1 [id id] (
    with_strategy l [id id] (
    with_strategy tl [id id] (
    with_strategy 0 [id id] (
    with_strategy transparent [id id] (
    with_strategy opaque [id id] (
    with_strategy expand [id id] (
    with_strategy 0 [idx] (
    with_strategy 0 [id x] (
    with_strategy 0 [x id] (
    with_strategy 0 [idn] (
    with_strategy 0 [idn x] (
    with_strategy 0 [idn id] (
    with_strategy 0 [idn id x] (
    with_strategy 0 [idan] (
    with_strategy 0 [idan x] (
    with_strategy 0 [idan id] (
    with_strategy 0 [idan id x] (
    idtac
      )))))))))))))))))).
  Print Ltac withstrategy.
End F.

Module FE := F E.
Print Ltac FE.withstrategy.