aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/CompactContexts.v
blob: 07588d34f9e6ca723d41a18f0904faecc1a0840f (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.