Ltac2's exact is less powerful than Ltac1's exact

[JasonGross]

Description of the problem

Existing Class True.
Existing Instance I.
Goal True. exact _. Qed.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.
Goal True. exact _. (* Error: Cannot infer this placeholder of type "True" (no type class instance
found).
*)

Perhaps exact needs to take preterm or whatever the Ltac2-equivalent of uconstr is and typecheck it with respect to the goal?

cc @ppedrot, is this solvable as Ltac2 currently stands, or do we need new primitives / types?

Coq Version

8.11

[Janno]

lazy_match! goal with [ |- ?g ] => let evar := open_constr:(_ : $g) in exact $evar end should work.

[Janno]

Oh, I realize the example is maybe a tad too minimal: you are looking for a way to allow arbitrary _ in the term?

[JasonGross]

Yes, and to write a tactic / tactic notation that has this behavior.

[ppedrot]

Indeed, exact should probably take a preterm. We don't have a lot of API for those yet, so before making these changes it might be better to implement the former.

[ppedrot]

Note that since then, the OCaml exact tactic was modified to take a glob_constr indeed. It's mostly a matter of exposing that to the Ltac2 world.