Tutorial outdated

[Matafou]

Hi there! I think a few hings can be updated in the tutorial, for a better experience.

1. The current version of the tutorial starts with a call to SearchAbout, which is now removed from last coq versions and is deprecated n favour of Search since a few versions.

2. The is a problem later on. Current versions of coq (at least 8.13 fail if the command following Fail fails to parse. Probably replacing Fail by Print would be ok.

Fail le.
Fail exfalso.

3. And finally near the end the following comment is probably outdated too but one needs to check in which version of coq the patched were added to official coq:

(** Here’s one final tip: with the right settings and a few patches to coqtop
    (available in coq-trunk), company-coq can also autocomplete externally
    defined symbols, tactics, and even tactic notations.  Once the patches are
    installed, you can enable these features by adding the following to your
    .emacs: (setq company-coq-live-on-the-edge t) *)