This gets rid of the old hack to have specific notations for pairs
up to a fixed arity, and moreover allows to do fancy things like:

```
Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.
```

This follows the associativity in Haskell. So, something like

  f <$> g <$> h

Is now parsed as:

  (f <$> g) <$> h

Since the functor is a generalized form of function application, this also now
also corresponds with the associativity of function application, which is also
left associative.

Infinity is described by having an injection from nat.

The documentation for some typeclasses used the wrong
names for these typeclasses.

This addresses some concerns in !5.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

This allows for more control over `Hint Mode`.

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None  m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None  m !! j = None.

That is, we have to specify the type of `m`.

See also Coq bug #5712.

Before, we often had to insert awkward casts when using them. Also,
the generality of also having them on Type, is probably not useful.

For example, instead of:

  Notation "( X ⊆ )"

We now use:

  Notation "( X ⊆)"

We were already doing this for = and ≡.

This solves some conflicts with the notations of MetaCoq.

Some were already maximally implicit, some were not. Now it is consistent.

This approach is originally by Robbert

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

Robbert Krebbers authored 8 years ago and Ralf Jung committed 8 years ago

We do this by introducing a type class UpClose with notation ↑.

The reason for this change is as follows: since `nclose : namespace
→ coPset` is declared as a coercion, the notation `nclose N ⊆ E` was
pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked
because type checking goes from left to right, and as such would look
for an instance `SubsetEq namespace`, which causes the right hand side
to be ill-typed.

Having Is_true as a type class caused problems with rewrite: when the
rewrited lemma has a premise of the shape Is_true, the rewrite tactic
will complain that it cannot find a type class instance, instead
of generating a goal for that premise.