Fix dead links to manual

README.md

@@ -40,7 +40,7 @@ If you have a trick you've found useful feel free to submit an issue or pull req
 - `intro`-patterns can be combined in a non-trivial way: `intros [=->%lemma]` -- see [IntroPatterns.v](src/IntroPatterns.v).
 - `change` tactic supports patterns (`?var`): e.g. `repeat change (fun x => ?f x) with f` would eta-reduce all the functions (of arbitrary arity) in the goal.
 - One way to implement a tactic that sleeps for n seconds is in [Sleep.v](src/Sleep.v).
-- Some tactics take an "[occurrence clause](https://coq.inria.fr/refman/proof-engine/tactics.html#occurrences-sets-and-occurrences-clauses)" to select where they apply. The common ones are `in *` and `in H` to apply everywhere and in a specific hypotheses, but there are actually a bunch of forms, for example:
+- Some tactics take an "[occurrence clause](https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/tactics.html#occurrence-clauses)" to select where they apply. The common ones are `in *` and `in H` to apply everywhere and in a specific hypotheses, but there are actually a bunch of forms, for example:
   - `in H1, H2` (just `H1` and `H2`)
   - `in H1, H2 |- *` (`H1`, `H2`, and the goal)
   - `in * |-` (just hypotheses)
@@ -58,7 +58,7 @@ If you have a trick you've found useful feel free to submit an issue or pull req
 - You can make all constructors of an inductive hints with `Hint Constructors`; you can also do this locally in a proof with `eauto using t` where `t` is the name of the inductive.
 - The `intuition` tactic has some unexpected behaviors. It takes a tactic to run on each goal, which is `auto with *` by default, using hints from _all hint databases_. `intuition idtac` or `intuition eauto` are both much safer. When using these, note that `intuition eauto; simpl` is parsed as `intuition (eauto; simpl)`, which is unlikely to be what you want; you'll need to instead write `(intuition eauto); simpl`.
 - The `Coq.Program.Tactics` library has a number of useful tactics and tactic helpers. Some gems that I like: `add_hypothesis` is like `pose proof` but fails if the fact is already in the context (a lightweight version of the `learn` approach); `destruct_one_ex` implements the tricky code to eliminate an `exists` while retaining names (it's a better version of our `deex`); `on_application` matches any application of `f` by simply handling a large number of arities.
-- You can structure your proofs using bullets. You [should use them in the order](https://coq.inria.fr/refman/proof-engine/proof-handling.html#bullets) `-`, `+`, `*` so that Proof General indents them correctly. If you need more bullets you can keep going with `--`, `++`, `**` (although you should rarely need more then three levels of bullets in one proof).
+- You can structure your proofs using bullets. You [should use them in the order](https://coq.inria.fr/doc/V8.19.0/refman/proofs/writing-proofs/proof-mode.html#bullets) `-`, `+`, `*` so that Proof General indents them correctly. If you need more bullets you can keep going with `--`, `++`, `**` (although you should rarely need more then three levels of bullets in one proof).
 - You can use the `set` tactic to create shorthand names for expressions. These are special `let`-bound variables and show up in the hypotheses as `v := def`. To "unfold" these definitions you can do `subst v` (note the explicit name is required, `subst` will not do this by default). This is a good way to make large goals readable, perhaps while figuring out what lemma to extract. It can also be useful if you need to refer these expressions.
 - When you write a function in proof mode (useful when dependent types are involved), you probably want to end the proof with `Defined` instead of `Qed`. The difference is that `Qed` makes the proof term opaque and prevents reduction, while `Defined` will simplify correctly. If you mix computational parts and proof parts (eg, functions which produce sigma types) then you may want to separate the proof into a lemma so that it doesn't get unfolded into a large proof term.
 - To make an evar an explicit goal, you can use this trick: `unshelve (instantiate (1:=_))`. The way this work is to instantiate the evar with a fresh evar (created due to the `_`) and then unshelve that evar, making it an explicit goal. See [UnshelveInstantiate.v](src/UnshelveInstantiate.v) for a working example.
@@ -79,11 +79,11 @@ If you have a trick you've found useful feel free to submit an issue or pull req
 - maximally inserted implicit arguments are implicit even when for identifier alone (eg, `nil` is defined to include the implicit list element type)
 - maximally inserted arguments can be defined differently for different numbers of arguments - undocumented but [`eq_refl` provides an example](https://github.com/coq/coq/blob/trunk/theories/Init/Logic.v#L297-298)
 - `r.(Field)` syntax: same as `Field r`, but convenient when `Field` is a projection function for the (record) type of `r`. If you use these, you might also want `Set Printing Projections` so Coq re-prints calls to projections with the same syntax.
-- `Function` vernacular provides a more advanced way to define recursive functions, which removes the restriction of having a structurally decreasing argument; you just need to specify a well-founded relation or a decreasing measure maps to a nat, then prove all necessary obligations to show this function can terminate. See [manual](https://coq.inria.fr/refman/language/gallina-extensions.html#coq:cmd.function) and examples in `Function.v` for more details.
+- `Function` vernacular provides a more advanced way to define recursive functions, which removes the restriction of having a structurally decreasing argument; you just need to specify a well-founded relation or a decreasing measure maps to a nat, then prove all necessary obligations to show this function can terminate. See [manual](https://coq.inria.fr/doc/V8.19.0/refman/using/libraries/funind.html#coq:cmd.Function) and examples in `Function.v` for more details.
 
   Two alternatives are considerable as drop-in replacements for `Function`.
 
-  - `Program Fixpoint` may be useful when defining a nested recursive function. See [manual](https://coq.inria.fr/refman/addendum/program.html#coq:cmd.program-fixpoint) and [this StackOverflow post](https://stackoverflow.com/questions/10292421/error-in-defining-ackermann-in-coq).
+  - `Program Fixpoint` may be useful when defining a nested recursive function. See [manual](https://coq.inria.fr/doc/V8.19.0/refman/addendum/program.html#program-fixpoint) and [this StackOverflow post](https://stackoverflow.com/questions/10292421/error-in-defining-ackermann-in-coq).
   - [CPDT's way](http://adam.chlipala.net/cpdt/html/Cpdt.GeneralRec.html) of defining general recursive functions with `Fix` combinator.
 
 - One can pattern-match on tuples under lambdas: `Definition fst {A B} : (A * B) -> A := fun '(x,_) => x.`