update readme

README.md

@@ -9,6 +9,9 @@ sound and complete: a program passes typechecking if and only if it is a well-ty
 program in MLTT. This will be the first verified proof assistant (despite being
 elementary) and serves as a basis for future extensions. 
 
+## Online Documentation
+
+We have generated a [Coqdoc](toc.html) for browsing our Coq proof.
 
 ## Architecture
 
@@ -67,19 +70,21 @@ opam install ppx_inline_test
 
 ## Development
 
-Before anything, the Coq parser must be extracted to OCaml code. Then, you can run `dune build` like normal for all other changes.
+Use the toplevel `make` to build the whole project:
+```
+make
+```
+Makefile will try to find out the number of your CPU cores and parallel as much as
+possible.
 
-You can build changes to the Coq parser with the following commands:
+Once `make` finishes, you can run the binary:
 ```
-cd theories
-make -j16 # or the number of your cpus
-cd ..
-dune build
+_build/default/driver/mcltt.exe examples/nary.mcl # or your own example
 ```
 
-Then you can interact with the parser at the toplevel with `dune utop`:
+To build Coq proof only, you can go into and only build the Coq folder:
 ```
-# open Mcltt;;
-# open Parser.Cst;;
-# Main.parse "<expression to parse>"
+cd theories
+make
 ```
+