coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?

From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?
Date: Tue, 10 Apr 2018 19:35:04 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f175.google.com
Ironport-phdr: 9a23:7ep4Hx2MFZAujRXusmDT+DRfVm0co7zxezQtwd8Zse0VL/ad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLniikHOT43/m/Ul8J+kr5UrQm9pxBj2YPYfJ2ZOOZ8c67bYNgURXBBXsFUVyFZB42zdYoOD/cBPeZZrIn9oEYFowakCgmvHuzvxSJIiWP23a07zu8sFhnG3A0jEt4SrnjZrs74NKgXUe+vzanIyS/PYO9R2Tf48YXFdA0qr/+LXbJ1a8XRyE8vGhvFjlWRtIPqIi2a1uIXv2iV9eVgVOavhmg6oA9yujii3tkghpXNi44PyV3J9T91zJs0KNGlUkJ3fNypHZtWuiqHLYV5WNkiTHttuCsiyr0Jp5q7fC8SxZQi3RHfaviHf5GI4xPtSOqdODl4iG9ndb+/nRqy/k+gyurzVsmwzllGtDZKkt7JtnwV1hzT7NaISudl80u/xTqC0xrf5+JELEwuiKbWKoMtzqQtmpcRsUnPBir2l1/3jK+SeEUk4O+o6+H/b7X+p5+RNJN4hh/8P6k1lcy/BP43MgkKX2SB5eu807jj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa7bmG9DGKmXJuLbnZ7d0rUBGmyQpytUKxJtGF7EAI/W7YUbyvdPFBR84e1iswra/UopV2YYXWGbJCaicZvCB+WSU7/4idrHfLLQevyzwfqB8tqzeyEQhkFpYRpGHmJ4eaXS2BPNjehzLbn/lg9NHGmAP7FNnEL7azWaaWDsWXE6cGrom72hiWo2jBIbHAIuqhe7ZhXrpLthtfmlDT2u0PzLoeoGDAalebSuTJopwjWRBW+H+Fsku0hahsAK8wL1ifLLZ

Sorry, last two lines of the attached file were wrong. The following
is correct, but the problem has not been solved yet.

Fail Extraction Inline A.hidden.
Fail Extract Constant A.hidden => "10".

2018-04-10 12:27 GMT+09:00 Kazuhiko Sakaguchi
<pi8027 AT gmail.com>:
> Hello,
>
> I tried to apply "Extraction Inline" and "Extraction Constant" for
> definitions hidden by using "Module Type" and "Module" in two ways,
> but both of them are failed. Do you have any idea for solving this?
>
> Best Regards,
> Kazuhiko

[Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?, Kazuhiko Sakaguchi, 04/10/2018
- Re: [Coq-Club] Can I apply "Extraction Inline" and "Extraction Constant" for definitions hidden by a module?, Kazuhiko Sakaguchi, 04/10/2018