blob: 652c65706a72c8555b0cc4c56486651b135ccb12 (
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 f 2.
intros s t.
refine
match t with
| v => s
end.
Defined.
Lemma test :
forall s, f s v = s.
Proof.
reflexivity.
Qed.
|
