aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2001.v
blob: d0b3bf173274e78aea96972338fa9bfadafce661 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(* Automatic computing of guard in "Theorem with"; check that guard is not
   computed when the user explicitly indicated it *)

Unset Automatic Introduction.

Inductive T : Set :=
| v : T.

Definition f (s:nat) (t:T) : nat.
fix 2.
intros s t.
refine
  match t with
  | v => s
  end.
Defined.

Lemma test :
  forall s, f s v = s.
Proof.
reflexivity.
Qed.