Поиск типов сигнатур типа модуля/модуля, на месте

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. 

Sure сообщение об ошибке, не говори мне ожидаемый тип ...

Я не» t знать, было ли это исправлено в 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. 

Ok ...

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