diff options
| author | XZ-X <x1456776728@icloud.com> | 2021-01-05 16:48:19 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-05 09:48:19 +0100 |
| commit | 73c49626476ed7ae4313f92431a9dea0b4eeb51d (patch) | |
| tree | 9555c19ef43e009e0362f8d1fe65f6207a778547 /README.md | |
| parent | 3d11e77273cfb6e10758ad242035e106f502fda8 (diff) | |
| download | smtcoq-73c49626476ed7ae4313f92431a9dea0b4eeb51d.tar.gz smtcoq-73c49626476ed7ae4313f92431a9dea0b4eeb51d.zip | |
Change imports from `SMTCoq` to `SMTCoq.SMTCoq` (#83)
* Update USE.md and `README.md`
Change the imports in `USE.md` and `README.md` from `SMTCoq` to `SMTCoq.SMTCoq`
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -16,7 +16,7 @@ SMTCoq is distributed under the CeCILL-C license. Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory. ```coq -Require Import SMTCoq ZArith. +Require Import SMTCoq.SMTCoq ZArith. Local Open Scope Z_scope. |