Print Module [Type] lacks types

Using Coq
1

Hello!

Consider this file:

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.FSets.FMaps.
Require Import Coq.FSets.FMapAVL.

Module StringMaps <: FMapInterface.S := FMapAVL.Make (String_as_OT).

Calling Print Module or Print Module Type on StringMaps shows useful information about the members of the module:

Module
StringMaps
 : Sig
     Module E
     Module Raw
     Record bst (elt : Type) : Type := Bst { this : Raw.t elt;  is_bst : Raw.bst this }.
     Definition this : forall elt : Type, bst elt -> Raw.t elt.
     Definition is_bst : forall (elt : Type) (b : bst elt), Raw.bst b.
     Definition t : Type -> Type.
     Definition key : Type.
     Definition empty : forall elt : Type, t elt.
...

However, because of the use of <: instead of :, the details of everything in the module is exposed to the world rather than being made nicely abstract. Switching to : in order to make large parts of the modue abstract, however, seems to make the various Print commands far less useful in a way that isn’t immediately apparent.

For example:

Module StringMaps : FMapInterface.S := FMapAVL.Make (String_as_OT).

Print Module StringMaps.
Module StringMaps : S := (Make String_as_OT)

Print Module Type StringMaps.
Module StringMaps : S

That’s fine, that’s what I’d expect. However…

Print Module Type S.
Result for command Print Module Type S . :

Module Type
 S =
 Sig
   Module E
   Definition key
   Parameter t
   Parameter empty
   Parameter is_empty
   Parameter add
   Parameter find
   Parameter remove

That’s not quite so useful. The types are missing.

The Check command will show the expected types of each member:

Check StringMaps.empty.
StringMaps.empty
     : forall elt : Type, StringMaps.t elt

Is there some other way to get a listing like the first one when a signature is used to restrict the view of a module like this? It’s very tedious to have to keep printing S and then looking up the individual definitions with Check, especially when I’m not sure which definition I need.