update readme

plclub · Jul 6, 2017 · bb10580 · bb10580
1 parent e68465a
commit bb10580
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 87 deletions.
diff --git a/Makefile b/Makefile
diff --git a/README.md b/README.md
@@ -3,9 +3,9 @@ COMPILATION, INSTALLATION, AND DOCUMENTATION:
   This library requires Coq 8.6, available via [opam](https://opam.ocaml.org/)
   or from the Coq website [https://coq.inria.fr/download].
 
-  To compile the library:
+  To compile the library, in the [Metalib](Metalib/) directory:
 
-     `make`          generate Coq makefile, compile Coq files
+     `make`           generate Coq makefile, compile Coq files
 	  `make html`     generate Coq documentation
 	  `make install`  install library on your system
 
@@ -16,9 +16,12 @@ TUTORIAL:
 
   The metatheory library comes with a short tutorial.  The main files for the
   tutorial are STLC.v, and STLCsol.v.  Make sure that you've compiled the
-  library first. The file [STLC.v](STLC.v) contains an introduction to
+  library first. The file [STLC.v](Tutorial/STLC.v) contains an introduction to
   mechanizing programming language definitions with binding in Coq and how to
-  reason about them.  Solutions to exercises are in [STLCsol.v](STLCsol.v).
+  reason about them.  Solutions to exercises are in [STLCsol.v](Tutorial/STLCsol.v).
+
+  An additional example of the library is available in the
+  [Fsub](Fsub/) directory.
 
   Those new to Coq should start with Software Foundations, which is an
   introduction to using Coq. The tutorial assumes some familarity with