From 73c49626476ed7ae4313f92431a9dea0b4eeb51d Mon Sep 17 00:00:00 2001
From: XZ-X <x1456776728@icloud.com>
Date: Tue, 5 Jan 2021 16:48:19 +0800
Subject: 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`
---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'README.md')

diff --git a/README.md b/README.md
index 236ef2f..d50afe0 100644
--- a/README.md
+++ b/README.md
@@ -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.
 
-- 
cgit