I want to write something like the following, but I get `Error: Cannot infer the implicit parameter A of eq_refl whose type is "Type".`

. It should be possible to infer all of the implicit arguments to `eq_refl`

because:

`my_refl _`

is matched against the`my_refl x`

appearing in the goal.- The type of
`my_refl x`

is`x = x`

. - The thing I'm changing
`my_refl x`

for should have the same type, so we should be trying to elaborate`eq_refl : x = x`

, which is fine.

How can I convey part 3 to Coq (without explicitly writing the type `x = x`

in my script)?

```
Definition my_refl {A} (x : A) : x = x := eq_refl.
Parameter A : Type.
Parameter x : A.
Goal my_refl x = eq_refl.
change (my_refl _) with eq_refl.
```

Here's the best I can come up with:

```
Definition my_refl {A} (x : A) : x = x := eq_refl.
Parameter A : Type.
Parameter x : A.
Goal my_refl x = eq_refl.
evar (ty : Type).
set (foo := my_refl _ : ty).
subst foo.
change (my_refl _) with (eq_refl : ty).
```

Or to not `subst foo.`

and instead `change foo with (eq_refl : ty).`

. It seems strange that `change`

doesn't just do this, though, and I also think there must be a way that's a little more direct.

or

```
set (foo := my_refl _);
let ty := type of foo in
let bar := open_constr:(eq_refl) in
let ty' := type of bar in
unify ty ty';
change foo with bar;
clear foo.
```

Can I extract this as an `Ltac`

definition (for arbitrary unelaborated terms instead of `my_refl _`

and `eq_refl`

)?

Aha, `Tactic Notation`

with `uconstr(...)`

arguments. Thanks!

James Wood has marked this topic as resolved.

Last updated: Jun 16 2024 at 02:41 UTC