Hi,

[EDIT (solved): apparently, it was just a matter of putting a `clear`

at a wrong place]

I'm writing a `Ltac`

tactic `tac`

such that:

- The first step of
`tac foo bar bar'`

is to produce a statement`H`

- The second step is asserting and proving
`H`

(namely with`let t := fresh "t" in assert (t:H)`

) - the third (would-be) step is outputting the proof-witness
`t`

of`H`

. I tried to do this with`exact t`

I'm pretty sure that step 1 and 2 are good.

When I try to do this on an example of the form:

` assert (try1 := ltac:(tac foo bar bar' ) ).`

I obtain the following error:

```
Cannot infer an existential variable of type "?T" in environment:
H := forall (x : Set) (x0 x1 : x) (x2 x3 : list x), x0 :: x2 = x1 :: x3 -> x0 = x1 /\ x2 = x3 /\ True : Prop
t : H
```

If I specify that the type of `try1`

is `H`

, I get the error: `The reference H was not found in the current environment.`

Is there a direct workaround to solve this ?

Christian Doczkal has marked this topic as resolved.

Last updated: Jan 29 2023 at 01:02 UTC