From eb892e63ecde76cba05a52f9b8f5cae7de680281 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 25 Nov 2024 14:23:30 +0100 Subject: [PATCH 1/3] coq export: use Require Export instead of Require Import --- src/export/coq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/export/coq.ml b/src/export/coq.ml index 8f9c584ee..f17c6dee6 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -355,7 +355,7 @@ let print : ast -> unit = fun s -> let oc = stdout in begin match !require with | Some f -> - string oc "Require Import "; + string oc "Require Export "; string oc (Filename.chop_extension f); string oc ".\n" | None -> () end; From 28542a967303354a23dd9d0b8e67150184656873 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 25 Nov 2024 20:12:34 +0100 Subject: [PATCH 2/3] wip --- doc/options.rst | 2 +- src/export/coq.ml | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/doc/options.rst b/doc/options.rst index 69c63c35d..ff7084691 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 `__. -* ``--requiring `` to add ``Require Import `` at the beginning of the output. ```` usually needs to contain at least the following definitions: +* ``--requiring `` to add ``Require Import `` at the beginning of the output. ```` usually needs to contain at least the following definitions: :: diff --git a/src/export/coq.ml b/src/export/coq.ml index f17c6dee6..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 Export "; - string oc (Filename.chop_extension f); string oc ".\n" + | Some f -> string oc ("Require Export "^f^".\n") | None -> () end; ast oc s From 4de842bdb123e33a9af5bf9c70af07aee9c4bde4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 25 Nov 2024 21:01:32 +0100 Subject: [PATCH 3/3] wip --- doc/options.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/options.rst b/doc/options.rst index ff7084691..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 `__. -* ``--requiring `` to add ``Require Import `` at the beginning of the output. ```` usually needs to contain at least the following definitions: +* ``--requiring `` to add ``Require Import `` at the beginning of the output. ``.v`` usually needs to contain at least the following definitions: ::