blob: 7d9f9eb2674a07f36f1b8b18d83e1d484b6501d6 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Test some uses of ? in introduction patterns *)
Inductive J : nat -> Prop :=
| K : forall p, J p -> (True /\ True) -> J (S p).
Lemma bug : forall n, J n -> J (S n).
Proof.
intros ? H.
induction H as [? ? [? ?]].
|