We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 10e5c4b commit 61d1287Copy full SHA for 61d1287
1 file changed
popl24/exercises/exercises.v
@@ -28,9 +28,15 @@
28
29
Define print_assumptions : global_env * term -> list kername
30
31
+**)
32
+
33
Load MetaCoqPrelude.
-(* if this does not work for you, compile the file using `coqc -I . "" MetaCoqPrelude`, and instead use the following line *)
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. *)
39
40
Require Import List.
41
42
Unset Guard Checking.
0 commit comments