We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 61d1287 commit 6e22b67Copy full SHA for 6e22b67
1 file changed
popl24/exercises/exercises.v
@@ -1,5 +1,14 @@
1
(*** MetaCoq Tutorial @ POPL 2024 ***)
2
3
+Load MetaCoqPrelude.
4
+(** If the above does not work for you, compile the file using
5
+ `coqc -I . "" MetaCoqPrelude` or using `make`
6
+ and use (uncomment) the following line instead
7
+**)
8
+(* Require Import MetaCoqPrelude. *)
9
+
10
+Require Import List.
11
12
(** EXERCISE ** Print Assumptions
13
14
A recent question on coq-club asked
@@ -30,15 +39,6 @@
30
39
31
40
**)
32
41
33
-Load MetaCoqPrelude.
34
-(** If the above does not work for you, compile the file using
35
- `coqc -I . "" MetaCoqPrelude` or using `make`
36
- and use (uncomment) the following line instead
37
-**)
38
-(* Require Import MetaCoqPrelude. *)
-
-Require Import List.
42
Unset Guard Checking.
43
Section fix_Σ.
44
0 commit comments