The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi Coq-Club !

I encountered a strange feature of Recursive Extraction (or Separate 
Extraction) while working with modules: it seems that, when a member of 
a module is to be extracted, the whole module is taken as a dependency.

Here is my example (tested in Coq 8.4pl1):

Module M.
Definition g (x:nat) := x.
Definition f (x:nat) := x.
End M.
Recursive Extraction M.f.

It returns:

type nat =
| O
| S of nat

module M =
 struct
  (** val g : nat -> nat **)

  let g x =
    x

  (** val f : nat -> nat **)

  let f x =
    x
 end

While I do not expect g to be extracted.

Is this a well-known behavior ? Is there any justification for that ? Is 
it a bug ?

In the same order of ideas, I would not expect a module to be extracted 
entirely while applied to a functor, but only the elements of the 
signature. The signatures used in functors parameters could be 
themselves stripped of unnecessary parts.

Thanks !
--
Jacques-Henri Jourdan