Bug 1572 - uninformative error message: Signature components ... do not match
: uninformative error message: Signature components ... do not match
Status: RESOLVED FIXED
Product: Coq
Classification: Unclassified
Component: Modules
: trunk
: All All
: P5 enhancement
: ---
Assigned To: Pierre Letouzey
Depends on:
Blocks:
  Show dependency treegraph
 
Reported: 2007-05-14 15:14 CEST by appel
Modified: 2013-03-21 22:26 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 appel 2007-05-14 15:14:27 CEST
Full_Name: Andrew Appel
Version: 8.1
OS: Windows
Submission from: aegis.cs.princeton.edu (128.112.139.195)


This error message is not very informative,
User error: Signature components for label t do not match

To see in what way it is not informative, consider that when I write "Locate t",
I get,

Constant Globalenvs.Genv.t
  (shorter name to refer to it in current context is Genv.t)
Constant Maps.NIndexed.t
  (shorter name to refer to it in current context is NIndexed.t)
Constant Maps.NMap.t
  (shorter name to refer to it in current context is NMap.t)
Constant W.Ownership.t
  (shorter name to refer to it in current context is Ownership.t)
Constant CME.W.Ownership.t
  (shorter name to refer to it in current context is CME.W.Ownership.t)
Constant Top.Cminor_Functor.CME.W.Ownership.t
  (shorter name to refer to it in current context is
Cminor_Functor.CME.W.Ownership.t)
Constant CMST.W.Ownership.t
  (shorter name to refer to it in current context is CMST.W.Ownership.t)
Constant CME.CMST.W.Ownership.t
  (shorter name to refer to it in current context is CME.CMST.W.Ownership.t)
Constant Top.Cminor_Functor.CME.CMST.W.Ownership.t
  (shorter name to refer to it in current context is
Cminor_Functor.CME.CMST.W.Ownership.t)
Constant Top.Cminor_Functor.CMST.W.Ownership.t
  (shorter name to refer to it in current context is
Cminor_Functor.CMST.W.Ownership.t)
Constant Top.Cminor_Functor.W.Ownership.t
  (shorter name to refer to it in current context is
Cminor_Functor.W.Ownership.t)
Constant Maps.PMap.t
  (shorter name to refer to it in current context is PMap.t)
Constant Maps.PTree.t
  (shorter name to refer to it in current context is PTree.t)
Constant Share.Share.t
  (shorter name to refer to it in current context is Share.Share.t)
Inductive CMST.State.t
  (shorter name to refer to it in current context is State.t)
Inductive CME.CMST.State.t
  (shorter name to refer to it in current context is CME.CMST.State.t)
Inductive Top.Cminor_Functor.CME.CMST.State.t
  (shorter name to refer to it in current context is
Cminor_Functor.CME.CMST.State.t)
Inductive Top.Cminor_Functor.CMST.State.t
  (shorter name to refer to it in current context is
Cminor_Functor.CMST.State.t)
Constant W.World.t
  (shorter name to refer to it in current context is World.t)
Constant CME.W.World.t
  (shorter name to refer to it in current context is CME.W.World.t)
Constant Top.Cminor_Functor.CME.W.World.t
  (shorter name to refer to it in current context is
Cminor_Functor.CME.W.World.t)
Constant CMST.W.World.t
  (shorter name to refer to it in current context is CMST.W.World.t)
Constant CME.CMST.W.World.t
  (shorter name to refer to it in current context is CME.CMST.W.World.t)
Constant Top.Cminor_Functor.CME.CMST.W.World.t
  (shorter name to refer to it in current context is
Cminor_Functor.CME.CMST.W.World.t)
Constant Top.Cminor_Functor.CMST.W.World.t
  (shorter name to refer to it in current context is
Cminor_Functor.CMST.W.World.t)
Constant Top.Cminor_Functor.W.World.t
  (shorter name to refer to it in current context is Cminor_Functor.W.World.t)
Constant Maps.ZIndexed.t
  (shorter name to refer to it in current context is ZIndexed.t)
Constant Maps.ZMap.t
  (shorter name to refer to it in current context is ZMap.t)

Comment 1 appel 2007-07-04 17:04:53 CEST
[ES]
Comment 2 Pierre Boutillier 2012-04-18 16:39:39 CEST
Pierre,

You are assignee just because I do not know the current situation ...

You can reses assignee to default if nothing has been done and you don't want to do it.
Comment 3 Pierre Letouzey 2013-03-21 22:26:37 CET
Wish granted in 8.4 and trunk (thanks Pierre-Marie !). For instance:

  Signature components for label x do not match: expected type
   "Impl1.T" but found type "Impl1'.T".

The display of this new error message used to fail on exception
such as Not_found due to non-robust term printers, but that should be
solved now (cf bug #3008).

Best Regards,
Pierre L.