_CoqProject 746 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
-Q exercises exercises
-Q solutions solutions
3
-Q talks/demo demo
4
5
6
7
8
9
10
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
# Can be triggered when importing some Iris files.
-arg -w -arg -notation-overridden

11
12
13
14
talks/demo/part1.v
talks/demo/part2.v
talks/demo/part3.v
talks/demo/part4.v
Hai Dang's avatar
Hai Dang committed
15
16
17
18
19
20
21
22
23
24
exercises/ex_01_swap.v
exercises/ex_02_sumlist.v
exercises/ex_03_spinlock.v
exercises/ex_04_parallel_add.v
exercises/ex_05_parallel_add_mul.v
solutions/ex_01_swap.v
solutions/ex_02_sumlist.v
solutions/ex_03_spinlock.v
solutions/ex_04_parallel_add.v
solutions/ex_05_parallel_add_mul.v