summaryrefslogtreecommitdiff
path: root/test-suite/output/CompactContexts.v
blob: c409c0ee46de5a28d0998edca9192f02cc36ebd3 (plain)
1
2
3
4
5
Set Printing Compact Contexts.

Lemma f (hP1:True) (a:nat) (b:list nat) (h:forall (x:nat) , { y:nat | y > x}) (h2:True): False.
Show.
Abort.