Does Ltac2 allocate a new evar for every antiquotation? (Things like `'($foo $bar)`

)

EDIT: it is `_`

's fault that an evar for the type is created.

```
From Ltac2 Require Import Ltac2.
Set Default Proof Mode "Classic".
Goal True.
unshelve ltac2:(let x := '(_) in ()); [| |].
```

~~seems to indicate that ~~`open_constr:`

creates an evar for the type (and the value, in this case).

no, `_`

with no type constraint does that

Oh, I see.

I guess Ltac2 is smart enough to not generate spurious evars, according to

```
Require Import Ltac2.Ltac2.
Goal True.
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := open_constr:(I) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
ltac1:(let v := constr:(I) in let w := open_constr:(v) in idtac).
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:($v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(ltac2:(Control.refine (fun () => v))) in ().
Optimize Proof. (* Evars: 3 -> 1 *)
let v := open_constr:(I) in let w := open_constr:(@conj True True $v $v) in ().
Optimize Proof. (* Evars: 1 -> 1 *)
```

Jason Gross has marked this topic as resolved.

why would it even generate an evar?

I vaguely recall the documentation saying something about how `$v`

is equivalent to `ltac2:(Control.refine (fun () => v))`

, which, if taken literally, suggests evar generation. And I have a vague sense that when I translate Ltac1 to Ltac2 without introducing anything unsafe, it gets a little bit slower, and was wondering if this could be a cause.

Last updated: May 20 2024 at 20:01 UTC