Coq extraction in separate modules

A.v

Inductive color := red | green | blue.

B.v

Require Import A.

Definition next_color (c : color) :=
  match c with
  | red => green
  | green => blue
  | blue => red
  end.

C.v

Require Import A.

Definition prev_color (c : color) :=
  match c with
  | red => blue
  | green => red
  | blue => green
  end.

Extract.v

Require Import A.
Require Import B.
Require Import C.

Require Extraction.
Extraction Language Haskell.
Extraction Library A.
Extraction Library B.
Extraction Library C.

This is the result:

A.hs:

module A where

import qualified Prelude

data Coq_color =
   Coq_red
 | Coq_green
 | Coq_blue

color_rect :: a1 -> a1 -> a1 -> Coq_color -> a1
color_rect f f0 f1 c =
  case c of {
   Coq_red -> f;
   Coq_green -> f0;
   Coq_blue -> f1}

color_rec :: a1 -> a1 -> a1 -> Coq_color -> a1
color_rec =
  color_rect

B.hs:

module B where

import qualified Prelude
import qualified A

next_color :: A.Coq_color -> A.Coq_color
next_color c =
  case c of {
   A.Coq_red -> A.Coq_green;
   A.Coq_green -> A.Coq_blue;
   A.Coq_blue -> A.Coq_red}

C.hs:

module C where

import qualified Prelude
import qualified A

prev_color :: A.Coq_color -> A.Coq_color
prev_color c =
  case c of {
   A.Coq_red -> A.Coq_blue;
   A.Coq_green -> A.Coq_red;
   A.Coq_blue -> A.Coq_green}