test-suite/output/bug_13238.v


1
2
3
4
5
6
7
8
9
10
11
12
13

Require Import ssreflect.

Ltac t1 x := replace (x x) with (x x).
Print t1.

Ltac t2 x := case: x.
Print t2.

Ltac t3 := by move->.
Print t3.

Ltac t4 := congr True.
Print t4.