From 40323e4258d5232226d0be277f53bb5462bac417 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 12 Sep 2019 11:41:28 +0200 Subject: Fix refine and eapply to mark shelved goals as non-resolvable, always Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals --- doc/changelog/04-tactics/10762-notypeclasses-refine.rst | 4 ++++ doc/sphinx/proof-engine/tactics.rst | 15 +++++++++------ 2 files changed, 13 insertions(+), 6 deletions(-) create mode 100644 doc/changelog/04-tactics/10762-notypeclasses-refine.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst new file mode 100644 index 0000000000..2fef75dc7f --- /dev/null +++ b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst @@ -0,0 +1,4 @@ +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and its variants no + longer allows shelved goals to be solved by typeclass resolution. + (`#10762 `_, by Matthieu Sozeau). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 81e50c0834..878118c48a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -555,12 +555,14 @@ Applying theorems This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are holes in the term. The type of holes must be either - synthesized by the system or declared by an explicit cast + subgoals as there are remaining holes in the elaborated term. The type + of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. This low-level tactic can be - useful to advanced users. + :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) + are *not* candidates for typeclass resolution, even if they have a type-class + type as conclusion, letting the user control when and how typeclass resolution + is launched on them. This low-level tactic can be useful to advanced users. .. example:: @@ -611,8 +613,9 @@ Applying theorems .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs type checking - without resolution of typeclasses. + This tactic behaves like the combination of :tacn:`simple refine` and + :tacn:`notypeclasses refine`: it performs type checking without resolution of + typeclasses, does not perform beta reductions or shelve the subgoals. .. flag:: Debug Unification -- cgit v1.2.3