The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

trying to write my own "Chlipala style" crush tactic, I came across the 
effect that eapply creates evars which don't have an existential hypothesis:

        Require Import Bool.
        Require Import Vector.

        Class BooleanEqualityT (T : Type) : Type :=
        {
            eqb       : T -> T -> bool ;
            eqb_axiom : forall x y, reflect (x = y) (eqb x y)
        }.

        Instance BooleanEquality_vector {T : Type} {Beq : BooleanEqualityT T} 
(n : nat) : BooleanEqualityT (Vector.t T n).
          eapply Build_BooleanEqualityT.

Results in:

        1 subgoal
        T : Type
        Beq : BooleanEqualityT T
        n : nat
        ______________________________________(1/1)
        forall x y : t T n, reflect (x = y) (?eqb x y)

The strange thing is that the evar ?eqb doesn't appear as existential in the 
hypothesis. This makes it difficult to detect the evar in automation and to 
set it.

So the question is: how can I detect in automation that I have such an evar 
and get its type?

Thanks & best regards,

Michael

P.S.: I am using Coq 8.5beta1 +  a few fixes.