blob: 93aeb83e28dbc5e4716a67d1a73b08d8b8362453 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Module NamedContext.
Definition foo := true.
Section Foo.
Let bar := foo.
Eval native_compute in bar.
Eval vm_compute in bar.
End Foo.
End NamedContext.
Module RelContext.
Definition foo := true.
Definition bar (x := foo) := Eval native_compute in x.
Definition barvm (x := foo) := Eval vm_compute in x.
End RelContext.
|
