@Pierre-Marie Pédrot : I have a weird effect with Ltac2 Eval. When I use it in a proof context, I get errors during Qed like

```
The variable X was not found in the current environment.
```

where X is a variable defined in the proof context.

Is this expected? Can one safely use Ltac2 Eval in a proof context? I do this sometimes to debug tactics which return a value.

example?

@Gaëtan Gilbert : a few 1000 lines of Ltac2 code - I first wanted to have an assesment if this is expected or not before I boild it down to something I can share.

Ltac2 Eval doc says it's supposed to be without side effect so not expected

not sure why it's not classified query tbh

OK, let me see if I can construct a short example

Here is a short example - it seems to have to do with mutable records:

```
Require Import Ltac2.Ltac2.
Ltac2 Type state := { mutable data : constr }.
Example Ex1: forall a : nat, True.
intros a.
Ltac2 Eval { data := 'a }.
exact I.
Qed.
```

Should I file a bug report?

Hmm - when I remove the `mutable`

it is still the same error.

this is probably the replay of side effect commands

What side effects would there be without the mutable?

eg

```
Require Import Ltac2.Ltac2.
Ltac2 Type state := { data : constr }.
Example Ex1: forall a : nat, True.
intros a.
Hint Resolve 0. (* outputs some warnings *)
exact I.
Qed. (* get the warnings again *)
```

Michael Soegtrop said:

What side effects would there be without the mutable?

there are no side effects, it's misclassified in the stm

open an issue

fix should be easy

OK, I will create an issue. Thanks!

even simpler example:

```
Require Import Ltac2.Ltac2.
Example Ex1: forall a : nat, True.
intros a.
Ltac2 Eval 'a.
exact I.
Qed.
```

Thanks, I will update the issue! (https://github.com/coq/coq/issues/15569)

https://github.com/coq/coq/pull/15570

Last updated: Jun 13 2024 at 03:02 UTC