The Coq mailing list

[Dan Christensen <jdc AT uwo.ca>]

On Nov 15, 2019, Samuel Gruetter 
<gruetter AT mit.edu>
 wrote:

> On Fri, 2019-11-15 at 23:13 +0100, Gaëtan Gilbert wrote:
>> probably one side uses a primitive projection and the other uses the 
>> compatibility constant
>> or both sides use the primitive projection but one is considered 
>> "unfolded" and the other isn't
>
> If that's indeed the source of the problem, you're in trouble Dan :(
> In bedrock2, we had to disable primitive projections because of this, but
> that comes at a cost...

How can I check whether this is what is going on?

The term looks like

  (fun x : X => smin (x, point Y))

Here Y is of type pType and the relevant definitions are

Class IsPointed (A : Type) := point : A.

Arguments point A {_}.

Record pType :=
  { pointed_type : Type ;
    ispointed_type : IsPointed pointed_type }.

The change tactic accepts replacing the term with the term I'm comparing
it to, so Coq does believe that they are convertible, and isn't that
what constr_eq is supposed to check?

(The unify tactic also fails to accept them as the same.)

Dan