I'm trying to update coq from 8.14.0 to 8.15.2 or 8.16.1. On both 8.15.2 and 8.16.1, however, I get error messages when i try to use `apply <some hypothesis> with (<argument name> := ...)`

. For example, when I have

```
H : forall (frame : nat) (x0 : list nat) (stk' : stack)
(v : nat) (stk2 : list nat),
aexp_frame_rule aexp fenv frame ->
(stk1 ++ x, c) = (stk', v) ->
stk1 ++ x = stk2 ++ x0 ->
stk' = stk2 ++ x0 ->
Datatypes.length stk2 = frame ->
forall x' : list nat,
aexp_stack_sem aexp fenv (stk2 ++ x') (stk2 ++ x', v)
```

in my context, and I try

```
eapply H with (stk2 := stk1) (x0 := x) (v := c) (stk' := stk1 ++ x) (x' := x') in H12.
```

I get the error

```
Error: No such bound variable stk2 (possible names are: frame, x, stk', v, stk1 and x').
```

(Also, `x`

, `stk'`

, `stk1`

, and `x'`

are all bound in the context. `v`

however is not, and only shows up as a quantified variable in `H`

.)

I've been able to use workarounds like `apply (<hypothesis name> <arguments>)`

, but there are still approximately 190 places where I would have to make changes, and I wouldn't be able to just use a find and replace to fix them because the arguments aren't always in order.

Is there a better way of doing this? I've been unable to find any information about this elsewhere. Additionally, I was TA-ing a class that used Coq, and multiple students had issues with this same problem as well.

`stk2`

is the renamed printing name of `stk1`

(you can tell from the "possible names are ..."

its real name is `stk1`

`apply`

stopped using the renamed names and uses the real names instead

this can be confusing but the previous behaviour was also a problem in other cases

Oh, thanks for letting me know! is there any way to see what the real names are/turn off the renaming of printing names?

for hypotheses it seems impossible other than relying on what the error tells you

otherwise `About H`

would work saying `Arguments H frame x stk' ...`

(ie if H is a definition or a section variable)

Last updated: Jun 24 2024 at 13:02 UTC