blob: 42573aad87c34560329cc9801a529a9be03dcf86 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* Check a few naming heuristics based on types *)
(* was buggy for types names _something *)
Inductive _foo :=.
Lemma bob : (sigT (fun x : nat => _foo)) -> _foo.
destruct 1.
exact _f.
Abort.
Inductive _'Foo :=.
Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo.
destruct 1.
exact _'f.
Abort.
Inductive ____ :=.
Lemma bob : (sigT (fun x : nat => ____)) -> ____.
destruct 1.
exact x0.
Abort.
|
