ensure all URLs have hyperlinks

README.md

@@ -96,7 +96,7 @@ To build all the examples in `src/`, run `make`.
 - `auto with foo nocore` with the pseudo-database `nocore` disables the default `core` hint databases and only uses hints from `foo` (and the context).
 - If you need to apply a theorem to a hypothesis and then immediately destruct the result, there's a concise way to do it without repetition: `apply thm in H as [x H]`, for example, might be used then `thm` produces an existential for a variable named `x`.
 - If you have a hypothesis `H: a = b` and need `f a = f b`, you can use `apply (f_equal f) in H`. (Strictly speaking this is just using the `f_equal` theorem in the standard library, but it's also very much like the inverse direction for the `f_equal` tactic.)
-- If you want to both run Ltac and return a `constr`, you can do so by wrapping the side effect in `let _ := match goal with _ => side_effect_tactic end in ...`. See https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884 for Jason Gross's much more thorough explanation.
+- If you want to both run Ltac and return a `constr`, you can do so by wrapping the side effect in `let _ := match goal with _ => side_effect_tactic end in ...`. See <https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884> for Jason Gross's much more thorough explanation.
 - If you want `lia` to help with non-linear arithmetic involving division or modulo (or the similar `quot` and `rem`), you can do that for simple cases with `Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.` See [DivMod.v](src/DivMod.v) for an example and the [micromega documentation](https://coq.github.io/doc/master/refman/addendum/micromega.html) the full details.
 - Coq's `admit` will force you to use `Admitted`. If you want to use Qed, you can instead use `Axiom falso : False. Ltac admit := destruct falso.` This can be useful for debugging Qed errors (say, due to universes) or slow Qeds.
 
@@ -184,7 +184,7 @@ To build all the examples in `src/`, run `make`.
 - You can use `all: fail "goals remaining".` to assert that a proof is complete. This is useful when you'll use `Admitted.` but want to document (and check in CI) that the proof is complete other than the `admit.` tactics used.
 - You can also use `Fail idtac.` to assert that a proof is complete, which is shorter than the above but more arcane.
 - You can use `Fail Fail Qed.` to really assert that a proof is complete, including doing universe checks, but then still be able to `Restart` it. I think this is only useful for illustrating small examples but it's amusing that it works. (The new `Succeed` vernacular in Coq 8.15 is a better replacement, because it preserves error messages on failure.)
-- Hints can now be set to global, export, or local. Global (the current default) means the hint applies to any module that transitivity imports this one; export makes the hint visible only if the caller imports this module directly. The behavior will eventually change for hints at the top-level so that they become export instead of global (see https://github.com/coq/coq/pull/13384), so this might be worth understanding now. [HintLocality.v](src/HintLocality.v) walks through what the three levels do.
+- Hints can now be set to global, export, or local. Global (the current default) means the hint applies to any module that transitivity imports this one; export makes the hint visible only if the caller imports this module directly. The behavior will eventually change for hints at the top-level so that they become export instead of global (see <https://github.com/coq/coq/pull/13384>), so this might be worth understanding now. [HintLocality.v](src/HintLocality.v) walks through what the three levels do.
 - The [uniform inheritance condition for coercions is
   gone](https://github.com/coq/coq/pull/15789) as of March 2022. This condition
   required that all the implicit arguments of the target of a coercion could be