Update export/README.md

1 files changed, 18 insertions, 18 deletions

diff --git a/export/README.md b/export/README.md
index 85e0790b..9b5d5b35 100644
--- a/export/README.md
+++ b/export/README.md
@@ -1,19 +1,23 @@
 # The clightgen tool
 
-
 ## Overview
-"clightgen" is an experimental tool that transforms C source files
-into Clight abstract syntax, pretty-printed in Coq format in .v files.
-These generated .v files can be loaded in a Coq session for
-interactive verification, typically.
 
+`clightgen` is an experimental tool that transforms C source files
+into Clight abstract syntax or Csyntax abstract syntax, pretty-printed
+in Coq format inside `.v` files.
+
+These generated `.v` files can be loaded in a Coq session for
+interactive verification, for example using the
+[VST](https://vst.cs.princeton.edu/) toolchain.
 
 ## How to build
 
-Change to the top-level CompCert directory and issue
-```
-   make clightgen
-```
+Configure CompCert with `./configure -clightgen`.
+
+Build CompCert as usual.
+
+The `clightgen` tool will be installed in the same directory as the
+`ccomp` compiler.
 
 ## Usage
 ```
@@ -22,12 +26,8 @@ Change to the top-level CompCert directory and issue
 For each source file `src.c`, its Clight abstract syntax is generated
 in `src.v`.
 
-The options recognized are a subset of those of the CompCert compiler ccomp
-(see [user's manual](http://compcert.inria.fr/man/manual003.html) for full documentation):
-```
-   -I<dir>     search <dir> for include files
-   -D<symbol>  define preprocessor macro
-   -U<symbol>  undefine preprocessor macro
-   -Wp,<opts>  pass options to C preprocessor
-   -f<feature> activate emulation of the given C feature
-```
+Run `clightgen -help` for a list of options.
+
+Several options are shared with the `ccomp` compiler; 
+see [user's manual](http://compcert.inria.fr/man/manual003.html)
+for full documentation).