Fix typos in the doc.

doc/sections/install.md

@@ -3,7 +3,7 @@ Installation via [Opam](http://opam.ocaml.org/)
 
 The version of `lambdapi` that is directly available through Opam (with the
 command `opam install lambdapi`) is currently outdated. We will only publish
-a new version of `lambdapi` Opam pacakge when the development has reached a
+a new version of `lambdapi` Opam package when the development has reached a
 more stable test. For now, we advise you to pin the development repository to
 get the latest bug fixes.
 

doc/sections/module.md

@@ -24,7 +24,7 @@ are cases where the files we want to work with are not (yet!) placed under the
 library root.  The typical case is when a library (or package) is still  under 
 development. In that case,  what we can do is map the development folder under
 the library root, similarly to what would happen when mounting a volume in our
-file system. There are two ways of doing that, the first one being to used the
+file system. There are two ways of doing that,  the first one being to use the
 `--map-dir MOD:DIR` command line option.  However, the best way is to use a
 package configuration file.
 
@@ -40,8 +40,8 @@ contain the following fields (an example is given below for the syntax):
  - `root_path` gives the module path under which the library is to be  placed.
    Assuming that our configuration file is at `<REPO_ROOT>/lambdapi.pkg`, this
    means that `<REPO_ROOT>/a/b/c.lp` will get module path `<ROOT_PATH>.a.b.c`.
-   In other words this is amounts to giving `--map-dir <ROOT_PATH>:<REPO_ROOT>`
-   on the command line.
+   In other words this is equivalent to `--map-dir <ROOT_PATH>:<REPO_ROOT>` on
+   the command line.
 
 In the future,  more useful meta data will be added to the configuration file,
 for example the name of the author, version number, dependencies, ...
@@ -57,7 +57,7 @@ key = value
 # There are two used keys for now:
 package_name = my_package_name
 root_path    = a.b.c
-# We will use more entries lated (e.g., authors, version, ...)
+# We will use more entries later (e.g., authors, version, ...)
 ```
 
 #### Installation procedure for third-party packages
@@ -73,7 +73,7 @@ we actually decide to implement automatic package distribution. For now, it is
 assumed that every user uses reasonable root paths for their packages.
 
 Note that if a package uses root path `a.b.c` then no other package should use
-root path `a` or `a.b` (and obvioulsy not `a.b.c` either). However there is no
+root path `a` or `a.b` (and obviously not `a.b.c` either). However there is no
 problem in using `a.d` or `a.b.d`. The rules are as follows:
  - the root path of a package cannot be a prefix of the root path of another,
  - the root path of a package cannot extend the root path of another.

doc/sections/options.md

@@ -51,8 +51,8 @@ command line arguments and flags.
 
  - `--lib-root DIR` sets the library root, that is, the folder corresponding
    to the entry point of the Lambdapi package system. This is the folder under
-   which every package is installed, and a default value is only only known if
-   Lambdapi has been installed. In development mode,  `--lib-root lib` must be
+   which every package is installed,  and a default value is only known if the
+   program has been installed.  In development mode,  `--lib-root lib` must be
    given (assuming Lambdapi is run at the root of the repository).
 
  - `--map-dir MOD:DIR` maps an arbitrary directory `DIR` under a module path
@@ -83,7 +83,7 @@ command line arguments and flags.
 
 Lambdapi provides an option `--confluence CMD` to check the confluence of the
 rewriting system by calling an external prover with the command `CMD`. The
-given command receives [TRS](http://project-coco.uibk.ac.at/problems/trs.php)
+given command receives [HRS](http://project-coco.uibk.ac.at/problems/hrs.php)
 formatted text on its standard input, and it is expected to output on the
 first line of its standard output either `YES`, `NO` or `MAYBE`.
 

doc/sections/structure.md

@@ -97,7 +97,7 @@ Structure of directories and files
    - `OK/`: tests that should succeed
    - `KO/`: tests that should fail
 
-* `lib/`: a minimal standar library for Lambdapi.
+* `lib/`: a minimal standard library for Lambdapi.
 
 * `tools/`:
    - `deps.ml`: gives the `#REQUIRE` commands that should be added at the beginning of a Dedukti file