blob: 12b0aa2cb5387b64b94360705c7963167902a40a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Coq.Program.Tactics.
(* these should not result in anomalies *)
Fail Program Lemma foo:
forall P, forall H, forall (n:nat), P n.
Fail Program Lemma foo:
forall a (P : list a -> Prop), forall H, forall (n:list a), P n.
Fail Program Lemma foo:
forall (a : Type) (P : list a -> Prop), forall H, forall (n:list a), P n.
|
