@Pierre-Marie Pédrot I try to write a function for `pose proof`

. I guess in Ltac2 Std.v the constructor `AssertValue (ident, constr)`

should get an `ident option`

to make this easy, or am I missing something?

This variant does work:

```
Require Import Ltac2.Ltac2.
Definition type_of {T : Type} (t : T) := T.
Ltac2 type_of (x : constr) := eval cbv beta delta [type_of] in (type_of $x).
Ltac2 pose_proof (proof_term : constr) :=
let proof_type := type_of proof_term in
assert ($proof_type) by exact $proof_term.
Goal True.
pose_proof constr:(I).
exact H.
Qed.
```

but I wonder why this one doesn't:

```
Ltac2 rct(x : constr) := Control.refine (fun () => x).
Ltac2 pose_proof' (proof_term : constr) :=
assert (ltac2:(rct (type_of proof_term))) by exact $proof_term.
```

It gives an error `The reference rct was not found in the current environment.`

which I don't understand. It looks like ltac2 doesn't work in the argument of `assert`

.

This is a parsing issue.

`assert (ltac2:(foo))`

is parsed as if you were willing to assert the hypothesis named `ltac2`

with type `foo`

.

It's one of the reasons I am not very fond of the current quotation system: it's very fragile from a parsing point of view.

FTR, you can work around this by adding a pair of parentheses around the ltac2:(...) quotations. It will force the parser to consider it as a Gallina term.

`assert (ltac2:(foo))`

is parsed as if you were willing to assert the hypothesis named`ltac2`

with type`foo`

.

Ah yes, I can see that it is tricky to get the `ltac2:`

parsed as I intended it.

It's one of the reasons I am not very fond of the current quotation system: it's very fragile from a parsing point of view.

Do you have a suggestion for an alternative which would be more robust?

Last updated: May 18 2024 at 10:02 UTC