search

arthuraa / deriving

Class instances for Coq inductive types with little boilerplate
MIT License
24 stars 9 forks source link

Unable to get deriving example to work #3

Closed zunction closed 4 years ago

zunction commented 4 years ago

Coq 8.10.2
mathcomp-ssreflect 1.9.0 coq-void 0.1.0

Trying to get run the README example running after having the above installed but run into error in Definition foo_eqMixin := Eval simpl in [derive eqMixin for foo]. with the error message Error: In environment x : phantom signature (base.PolyType.cons (base.PolyType.cons (NonRec nat) base.PolyType.nil) base.PolyType.nil) The term "x" has type "phantom signature (base.PolyType.cons (base.PolyType.cons (NonRec nat) base.PolyType.nil) base.PolyType.nil)" while it is expected to have type "phantom signature ?sΣ".

Any ideas what I'm missing to get the error? Thanks

arthuraa commented 4 years ago

Good catch! The example was missing an import. I just corrected it; it should be working now.