This is needed to use coq-stdpp in developments with -type-in-type
as set_unfold will otherwise unify with any hyp, causing the
set_solver tactic to break.

This way, we get more definitional equalities.

To be consistent with Iris, see Iris commit 9ee62b3a.

This partially reverts 2bf11f4f.  There is no need to add new Makefile targets as the Makefile already forwards all targets to Makefile.coq.

It is sometimes not desirable to do so.

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.

To make it consistent with Forall_impl and map_Forall_impl. Also, put
the premises in the same order as those lemmas.

also add html folder to .gitignore so generated doc is not added to the repo