_CoqProject 876 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
-Q solutions solutions
Robbert Krebbers's avatar
Robbert Krebbers committed
2
-Q exercises exercises
3
4
# Iris 3.3 still uses this to be compatible with Coq 8.9.
-arg -w -arg -convert_concl_no_check
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
solutions/language.v
solutions/polymorphism.v
solutions/types.v
solutions/typed.v
solutions/sem_types.v
solutions/sem_type_formers.v
solutions/sem_typed.v
solutions/sem_operators.v
solutions/compatibility.v
solutions/fundamental.v
solutions/safety.v
solutions/two_state_ghost.v
solutions/symbol_ghost.v
solutions/unsafe.v
solutions/parametricity.v
solutions/interp.v
Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
exercises/language.v
exercises/polymorphism.v
exercises/types.v
exercises/typed.v
exercises/sem_types.v
exercises/sem_type_formers.v
exercises/sem_typed.v
exercises/sem_operators.v
exercises/compatibility.v
exercises/fundamental.v
exercises/safety.v
exercises/two_state_ghost.v
exercises/symbol_ghost.v
exercises/unsafe.v
exercises/parametricity.v
exercises/interp.v