wip

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>`` usually needs to contain at least the following definitions:
 
 ::
 

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 Export ";
-      string oc (Filename.chop_extension f); string oc ".\n"
+  | Some f -> string oc ("Require Export "^f^".\n")
   | None -> ()
   end;
   ast oc s