[EDIT (solved): apparently, it was just a matter of putting a
clearat a wrong place]
I'm writing a
tac foo bar bar'is to produce a statement
let t := fresh "t" in assert (t:H))
H. I tried to do this with
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
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: Sep 28 2023 at 10:01 UTC