coq

coq copied to clipboard

As shown in #16935, the interpretation of references in Ltac functions happens to be different in strict mode (i.e., in practice, non interactively) and in non-strict mode (i.e., in practice, interactively) regarding the insertion or not of maximal implicit arguments.

This comment at #16935 suggested to align the strict mode on the non-strict mode and this is what the PR does.

In particular, this ensures than in a configuration such as:

Class T.
Local Instance t : T := {}.
Parameter a : forall {t:T}, True.
Ltac f x := exact x.
Ltac g := f a.
Goal True.
g.

where g evaluates an Ltac function applied to a reference in strict mode and this reference has inferable maximal implicit arguments, the implicit arguments are indeed inserted, as if f a had been given directly.

I did not find other cases where the change of semantics is observable (i.e. the maximal implicit arguments need to be solvable by type class inference, otherwise it fails with an unresolved implicit arguments anyway). In the stdlib, the only occurrence of such pattern is class_apply (which plays the role of f above) and the compatibility can be preserved by turning class_apply into a tactic definition.

• [ ] Added changelog.
• [ ] Added / updated documentation.