2 files changed, 7 insertions, 7 deletions
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.
 
diff --git a/USE.md b/USE.md
index 7aa4b3b..d9e9ad5 100644
--- a/USE.md
+++ b/USE.md
@@ -14,7 +14,7 @@ easily re-usable for your own usage.
 ## Overview
 
 After installation, the SMTCoq module can be used in Coq files via the
-`Require Import SMTCoq.` command. For each supported solver, it
+`Require Import SMTCoq.SMTCoq.` command. For each supported solver, it
 provides:
 
 - a vernacular command to check answers: `XXX_Checker "problem_file"
@@ -60,7 +60,7 @@ To check the result given by zChaff on an unsatisfiable dimacs file
 
 - In a Coq file `file.v`, put:
 ```coq
-Require Import SMTCoq.
+Require Import SMTCoq.SMTCoq.
 Zchaff_Checker "file.cnf" "resolve_trace".
 ```
 
@@ -70,7 +70,7 @@ Zchaff_Checker "file.cnf" "resolve_trace".
 - You can also produce Coq theorems from zChaff proof witnesses: the
   commands
 ```coq
-Require Import SMTCoq.
+Require Import SMTCoq.SMTCoq.
 Zchaff_Theorem theo "file.cnf" "resolve_trace".
 ```
 will produce a Coq term `theo` whose type is the theorem stated in
@@ -111,7 +111,7 @@ This command produces a proof witness file named `file.log`.
 
 - In a Coq file `file.v`, put:
 ```coq
-Require Import SMTCoq.
+Require Import SMTCoq.SMTCoq.
 Section File.
   Verit_Checker "file.smt2" "file.log".
 End File.
@@ -123,7 +123,7 @@ End File.
 - You can also produce Coq theorems from veriT proof witnesses: the
   commands
 ```coq
-Require Import SMTCoq.
+Require Import SMTCoq.SMTCoq.
 Section File.
   Verit_Theorem theo "file.smt2" "file.log".
 End File.
@@ -186,7 +186,7 @@ This set of commands produces a proof witness file named `name.lfsc`.
 
 - In a Coq file `name.v`, put:
 ```coq
-Require Import SMTCoq Bool List.
+Require Import SMTCoq.SMTCoq Bool List.
 Import ListNotations BVList.BITVECTOR_LIST FArray.
 Local Open Scope list_scope.
 Local Open Scope farray_scope.