summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5741.v
blob: f6598f192d2fc7f597c3eff553ef1830e2f0220f (plain)
1
2
3
4
(* Check no anomaly in info_trivial *)

Goal True.
info_trivial.