1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* info auto: *)
simple apply or_intror (in core).
intro.
assumption.
(* debug auto: *)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply or_intror (in core). (*success*)
** assumption. (*fail*)
** intro. (*success*)
** assumption. (*success*)
(* info eauto: *)
simple apply or_intror.
intro.
exact H.
(* debug eauto: *)
Debug: 1 depth=5
Debug: 1.1 depth=4 simple apply or_intror
Debug: 1.1.1 depth=4 intro
Debug: 1.1.1.1 depth=4 exact H
(* info trivial: *)
exact I (in core).
|
