Rename `f_contractive_core` into `dist_later_intro`.
This MR is based on !886 (merged), so that one needs to be merged first.
In actris!29 (merged) I realized that it is sometimes necessary to apply
a Contractive
instance yourself. After that, you have a goal of the form dist_later
. The tactic f_contractive_core
is very useful to introduce such goals, but it currently appears to be intended as an implementation detail. This MR:
- Renames
f_contractive_core
intodist_later_intro
so that it becomes a proper tactic that downstream users could use. - Removes the
try
from its definition so that it only succeeds if the goal is actually adist_later
. Thetry
has been moved tof_contractive
. - Provides versions
dist_later_intro as n Hn
anddist_later_intro
without arguments, following the same syntax asf_contractive
. - Does the same for
f_contractive_fin_core
. - Tweaks the documentation accordingly.