Bug 2466 - "Error: Signature components for label ... do not match." doesn't include actual or expected types
: "Error: Signature components for label ... do not match." doesn't include act...
Status: RESOLVED FIXED
Product: Coq
Classification: Unclassified
Component: Modules
: 8.3
: All All
: P5 enhancement
: ---
Assigned To: nobody
Depends on:
Blocks:
  Show dependency treegraph
 
Reported: 2010-12-30 12:17 CET by Ian Lynagh
Modified: 2013-02-24 21:30 CET (History)
1 user (show)

See Also:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Ian Lynagh 2010-12-30 12:17:53 CET
The code below gives this error:

Error: Signature components for label eq_equiv do not match.

I would like the error to include 'nat' and whatever the expected type is.

I have v8.3 (13702).



Require Import MSetWeakList.

Parameter Name : Set.
Axiom eq_Name_dec : forall (n : Name) (o : Name),
                    {n = o} + {n <> o}.

Module DecidableName.
Definition t := Name.
Definition eq := @eq Name.
Definition eq_dec := eq_Name_dec.
Definition eq_equiv := 1.
End DecidableName.

Module NameSetMod := Make(DecidableName).
Comment 1 Pierre-Marie Pédrot 2013-02-24 21:30:21 CET
Fixed in trunk.