The Coq mailing list

[刘坚 <liujian AT ios.ac.cn>]

Hi all,

Currently we are developing a formal verification tool based on coq.

Here is the background:

There exist many .v files for a project, one for each C function. So when we were generating proof of a C function, it is reasonably needed to “Require Import” all proofs of its calling functions.

Suppose that: each proof script contains both the definition of a C function and the definition of its proof term.

The problem is that: in practice, when we are “Require Import”ing a proof, all we want to import is the proof term defined, not the C function definition. Because otherwise, according to the semantics of “Require Import”, the size of vo of a top level function
 with very deep nesting of sub function calls will be very large. We want to import the necessary constants only.

Here is the question:

Is there any way to import constants in an selective way? If not, could you please introduce me some materials about the libobject module in the src of coq? Because I am currently reading the source code but got stuck on this module. As far as I know, it will
 be very helpful to understand libobject before I can solve my problem.

Could you please give me some suggestions?

Thank you!

Best,
Jian