Updated README

Author: monadius

README.md

@@ -15,23 +15,46 @@ Run `make .merlin` to create the `.merlin` file.
 
 ## New Vernacular Commands
 
-- `CWTest string? qualid Assumes qualid*`
+- `CWAssert string? qualid Assumes qualid*`
 
    This command fails if the tested `qualid` depends on an axiom which is not listed after `Assumes`:
 
    ```coq
-   CWTest "Testing lemma" lemma Assumes proof_irrelevance functional_extensionality.
+   CWAssert "Testing lemma" lemma Assumes proof_irrelevance functional_extensionality.
    ```
-   The string argument after `CWTest` is an optional message.
+   The string argument after `CWAssert` is an optional message.
+
+- `CWAssert string? qualid : term`
+
+   Checks if the type of `qualid` is convertible to the type given by `term`.
+
+   ```coq
+   CWAssert "Testing type" lemma : (forall x, x > 0).
+   ```
+   The string argument after `CWAssert` is an optional message.
+
+   Note that the `term` should be in parentheses.
 
 - `CWGroup string`
 
-   Begins a group of tests.
+   Begins a group of tests (outputs `<DESCRIBE::>`).
+
+   Groups can be nested. But all tests should be performed after `CWTest` in nested groups.
 
 - `CWEndGroup`
 
    Ends a group of tests.
 
+- `CWTest string`
+
+   Begins a test case (outputs `<IT::>`).
+
+   Test cases cannot be nested.
+
+- `CWEndTest`.
+
+   Ends a test case. This command is optional before `CWTest` and `CWEndGroup`.
+
 - `CWFile string? Size < int`
 
    Tests if the size of a file (the first string argument) is less than the second argument.
@@ -48,8 +71,9 @@ Run `make .merlin` to create the `.merlin` file.
 
 ## Examples
 
-See [theories/Demo.v](theories/Demo.v) and [theories/Demo2.v](theories/Demo2.v)
-for more examples.
+See [cw_example/SolutionTest.v](cw_example/SolutionTest.v).
+
+More examples are in [theories/Demo.v](theories/Demo.v) and [theories/Demo2.v](theories/Demo2.v).
 
 Compiling demo files:
 ```