ssreflect - [ssreflect] Coqchk output

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Coqchk output

From: Felipe Cerqueira <>
To: "" <>
Subject: [ssreflect] Coqchk output
Date: Wed, 4 May 2016 11:43:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:B9WpfBIaNPI48B3cWtmcpTZWNBhigK39O0sv0rFitYgUIvnxwZ3uMQTl6Ol3ixeRBMOAu6MC07Od6vu6EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxj7n5osaJKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvCwZL8iQLJcAT86G2Uu/ojqswPCRE2O4GEdWyMYiFAAVxPe9hz0Wpr6rgP/rfA42S+APMSwTLYuWD3k4b09GzHyjyJSGTM98Xnawud9lrtGrRO7rlQrzYPQYZmYP9J7ZqKYZswBA21bUZACBGR6HoqgYt5XXKI6NuFCotylqg==

Hi everyone,

I have a simple question about the coqchk output when importing ssreflect.
It seems to contain many Axioms from module types:

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
Ssreflect.fintype.SubsetDef.subsetEdef    
Ssreflect.fintype.SubsetDef.subset    
MathComp.tuple.FinTuple.size_enum    
MathComp.finfun.FunFinfun.fun_of_finE    
MathComp.finfun.FunFinfun.fun_of_fin    
MathComp.finfun.FunFinfun.finfunE    
MathComp.finfun.FunFinfun.finfun     
MathComp.tuple.FinTuple.enumP    
Ssreflect.fintype.Finite.EnumDef.enumDef    
MathComp.tuple.FinTuple.enum    
Ssreflect.fintype.Finite.EnumDef.enum    
Ssreflect.fintype.CardDef.cardEdef    
Ssreflect.fintype.CardDef.card    
MathComp.bigop.BigOp.bigopE    
MathComp.bigop.BigOp.bigop

Is this a problem with coqchk? Is there a way to get rid of that?

Thanks,
Felipe

[ssreflect] Coqchk output, Felipe Cerqueira, 05/04/2016
- Re: [ssreflect] Coqchk output, Enrico Tassi, 05/04/2016
  - Re: [ssreflect] Coqchk output, Felipe Cerqueira, 05/04/2016
    - Re: [ssreflect] Coqchk output, Felipe Cerqueira, 05/05/2016

List archive

[ssreflect] Coqchk output