The Coq mailing list

[Daniel Sch�ssler <danlex AT gmx.de>]

Hello Coq-Club!

for reference:
=================================
$ About inj_pairT2.
Notation inj_pairT2 := inj_pair2

$ About inj_pair2.
inj_pair2 :
forall (U : Type) (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = y

Expands to: Constant Coq.Logic.Eqdep.EqdepTheory.inj_pair2

$ Print HintDb core.
...
For eq -> ...
            eapply Eqdep.EqdepTheory.inj_pairT2(2)
            eapply Eqdep.EqdepTheory.eq_dep_eq(2)
...
=================================

There are several problems with this:
- Very general conclusion.
- Premise matches conclusion, leading to looping.
- It's in the 'core' db, so (as far as I'm aware) you can't turn it off.
- Eqdep is exported by quite a few other modules, such as SetoidClass and 
Program.

any workarounds? Maybe it should be considered to move this out of 'core' 
:)


Greetings,
Daniel