diff --git a/doc/options.rst b/doc/options.rst
index 69c63c35d..f614aa072 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -122,7 +122,7 @@ In symbol declarations or definitions, parameters with no type are assumed to be
 
 It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``coq_expr``, which can be any Coq expression. Example: `renaming.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/renaming.lp>`__.
 
-* ``--requiring <COQ_FILE>`` to add ``Require Import <COQ_FILE>`` at the beginning of the output. ``<COQ_FILE>`` usually needs to contain at least the following definitions:
+* ``--requiring <MODNAME>`` to add ``Require Import <MODNAME>`` at the beginning of the output. ``<MODNAME>.v`` usually needs to contain at least the following definitions:
 
 ::
 
diff --git a/src/export/coq.ml b/src/export/coq.ml
index 8f9c584ee..1d6552db0 100644
--- a/src/export/coq.ml
+++ b/src/export/coq.ml
@@ -354,9 +354,7 @@ let set_requiring : string -> unit = fun f -> require := Some f
 let print : ast -> unit = fun s ->
   let oc = stdout in
   begin match !require with
-    | Some f ->
-      string oc "Require Import ";
-      string oc (Filename.chop_extension f); string oc ".\n"
+  | Some f -> string oc ("Require Export "^f^".\n")
   | None -> ()
   end;
   ast oc s