The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I have a .v file that has as its only contents:

Require Export EquivDec.

Class Ordered(A : Set) :=
  {
    eq_dec :> EqDec A eq;
    lt : A -> A -> Prop;
    lt_strict :> StrictOrder lt;
    compare : A -> A -> comparison;
    compare_spec : forall x y, CompareSpecT (eq x y) (lt x y) (lt y x) 
(compare x y)
  }.

Print Assumptions Ordered.


The last Print Assumptions outputs "Closed under the global context".

When I run that file through coqchk with the -o option, it prints this 
at the end:

* Axioms:
    Coq.Logic.ProofIrrelevance.proof_irrelevance
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.Logic.JMeq.JMeq_eq
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq


Why is coqchk seeing those axioms when Print Assumptions isn't?  The 
difference isn't due to the use of "Export" - as I tried "Import" 
instead with the same results.

-- Jonathan