Documentation

INSTALL.md

@@ -249,14 +249,18 @@ The `zchaff` binary must be present in your PATH to use it through SMTCoq.
 ## Setting up environment for SMTCoq
 ### Using SMTCoq without installing
 
-If you want to use SMTCoq without installing it your Coq installation, you can
+If you want to use SMTCoq without adding it to your Coq installation, you can
 tell Coq where to find SMTCoq by adding the following line in the file
 `~/.config/coqrc`:
 
 ```coq
 Add Rec LoadPath "~/path/to/smtcoq/src" as SMTCoq.
 ```
 
+See [this
+documentation](https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file)
+if it does not work.
+
 
 ### Emacs and ProofGeneral
 

README.md

@@ -105,7 +105,7 @@ The `zchaff` tactic can be used to solve any goal of the form:
 ```coq
 forall l, b1 = b2
 ```
-where `l` is a quantifier-free list of variables and `b1` and `b2` are
+where `l` is a quantifier-free list of terms and `b1` and `b2` are
 expressions of type `bool`.
 
 A more efficient version of this tactic, called `zchaff_no_check`,
@@ -164,10 +164,12 @@ The `verit_bool [h1 ...]` tactic can be used to solve any goal of the form:
 ```coq
 forall l, b1 = b2
 ```
-where `l` is a quantifier-free list of variables and `b1` and `b2` are
+where `l` is a quantifier-free list of terms and `b1` and `b2` are
 expressions of type `bool`. This tactic *supports quantifiers*: it takes
 optional arguments which are names of universally quantified
-lemmas/hypotheses that can be used to solve the goal.
+lemmas/hypotheses that can be used to solve the goal. These lemmas can
+also be given once and for all using the `Add_lemmas` command (see
+examples/Example.v for details).
 
 In addition, the `verit` tactic applies to Coq goals of sort `Prop`: it
 first converts the goal into a term of type `bool` (thanks to the