找到模塊/模塊類型的類型簽名，在適當的位置

Question

這個問題一直在困擾着我很多次。有沒有辦法在Coq中打印模塊類型中每個元素的簽名。

例如：

Print Orders.OrderedType. 

Module Type Orders.OrderedType = Sig 
           Parameter t 
           Parameter eq 
           Parameter eq_equiv 
           Parameter lt 
           Parameter lt_strorder 
           Parameter lt_compat 
           Parameter compare 
           Parameter compare_spec 
           Parameter eq_dec 
          End 

---

Print Module Type Orders.OrderedType. 

Module Type Orders.OrderedType = Sig 
           Parameter t 
           Parameter eq 
           Parameter eq_equiv 
           Parameter lt 
           Parameter lt_strorder 
           Parameter lt_compat 
           Parameter compare 
           Parameter compare_spec 
           Parameter eq_dec 
          End 

---

About Orders.OrderedType. 

Module Type Coq.Structures.Orders.OrderedType 

---

所有這些都是無用的，因爲他們不提醒我每個元素的類型...

我甚至不能使用錯誤信息提醒我，因爲他們是愚蠢的：

Error: Signature components for label eq do not match. 

當然錯誤信息，不要告訴我預期的類型......

我不不知道這個問題是否已經在8.4中得到了解決，但我真的很喜歡這樣一種方法，不必去查看這個定義的位置，以便提醒它是如何定義的。有這樣的事嗎？ :(

---

特別是查不到的定義只是沿着模塊組合的可笑長鏈追逐......嚴重：

Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec. 

好的，謝謝......

Module Type DecStrOrder := StrOrder <+ HasCompare. 

繼續...

Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder. 

...

Module Type EqualityType := Eq <+ IsEq. 

當然...

Module Type Eq := Typ <+ HasEq. 

好吧......

Module Type Typ. 
    Parameter Inline(10) t : Type. 
End Typ. 

最後，我知道的t類型！ \ o/

Answer 1

作爲一個部分答案，這似乎在過去的一個月裏在主幹中得到了修復。參看

http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1572

和

http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2466