blob: 325ee95ae246b7e2f707819cf92147745f16ea10 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
Extracted code successfully compiled
type __ = Obj.t
type unit0 =
| Tt
type bool =
| True
| False
module Case1 =
struct
type coq_rec = { f : bool }
(** val f : bool -> coq_rec -> bool **)
let f _ r =
r.f
(** val silly : bool -> coq_rec -> __ **)
let silly x b =
match x with
| True -> Obj.magic b.f
| False -> Obj.magic Tt
end
module Case2 =
struct
type coq_rec = { f : (bool -> bool) }
(** val f : bool -> coq_rec -> bool -> bool **)
let f _ r =
r.f
(** val silly : bool -> coq_rec -> __ **)
let silly x b =
match x with
| True -> Obj.magic b.f False
| False -> Obj.magic Tt
end
|
