Instructions for setting up PLF ------------------------------- 1) Download and extract the plf.zip file from the course website. 2) Inside the plf directory you should find the following files: _CoqProject Preface.v Maps.v Imp.v Equiv.v 3) This is the directory where you should be putting any new files, starting with Hoare.v. 4) To compile these files you can follow the instructions in the Basics.v file from LF to create a Makefile, or just manually compile the four modules: coqc -Q . PLF Preface.v coqc -Q . PLF Maps.v coqc -Q . PLF Imp.v coqc -Q . PLF Equiv.v