Ltac2 Notation refine missing arg?

[jonleivent]

Coq v8.12.2
In Ltac2/Notations.v, refine is defined as:

Ltac2 Notation refine := Control.refine.

Should it be this instead?:

Ltac2 Notation refine c(thunk(open_constr)) := Control.refine c.

so that the syntax of refine calls mirrors Ltac1, as with other Ltac2 notations?

[ppedrot]

It's a legitimate question that has a borderline answer. Ltac2 lets you write quoted terms easily as 'foo or '(foo) depending on the shape. The cost of adding a notation is quite important because it modifies the parser and prevents calls to other functions that would be called refine. Meanwhile, adding a quote is not very costly. Therefore, I decided that for Ltac2 functions that were identifiers followed by constr entries, it was probably better to stick to the convention that they are grammar-free definitions.

[samuelgruetter]

I can see @ppedrot's point, but I'll add an example that puzzled me quite a bit: Coming from Ltac1, I was expecting that the following should work:

Goal 2 = 2.
  refine (f_equal S _).

However, I got a syntax error:

Error: Syntax error: ')' or ':' expected after [ltac2_expr] (in [ltac2_expr]).

The fix is as simple as adding a ':

  refine '(f_equal S _).

Moreover, exact eq_refl. works, whereas refine eq_refl. fails with Error: Unbound value eq_refl, and needs to be written as refine 'eq_refl. instead. So the notation for exact already doesn't respect @ppedrot's argument, so why not change refine to behave like exact?

[ppedrot]

Exact is a bit different for reasons that do not hold currently. In theory, it should take an untyped constr rather than a constr as an argument, to be able to cast it to the type of the goal.

[SkySkimmer]

Exact is a bit different for reasons that do not hold currently. In theory, it should take an untyped constr rather than a constr as an argument, to be able to cast it to the type of the goal.

But refine should do the same thing IMO