[WIP] Fixes for compatibility with Coq v8.10 and master

[tchajed]

I've tested this on Coq v8.9.1, v8.10.1, and the current Coq master.

An incomplete list of changes needed:

• Coq now generates slightly different files, which requires new gitignore rules.
• Instances can no longer be partially provided with := (so that it's syntactically obvious whether or not we're in proof mode). The relevant change to Coq for InteractionTrees is https://github.com/coq/coq/pull/9270.
• The projection syntax now only supports record projections (see https://github.com/coq/coq/pull/8829). This is a bit sad since it would be nice for the user to think of observe as a projection; hopefully Coq supports that in some way.

There was one mysterious breakage in Eq/UpToTaus.v. The rewrite previously there now goes into an infinite loop while resolving typeclasses for setoid rewriting. I managed to fix it by essentially manually giving the right instance, but it would be nice to fix the underlying issue.

[tchajed]

Oops, this seemed to work but I ran into another rewrite infinite loop in tutorial/AsmCombinators.v.

[Lysxia]

I ended up fixing compatibility with 8.10 independently in #153 (from a branch that was dormant prior to this PR). I'll borrow your first commit for the gitignore as part of adding Coq master to CI (WIP on branch coq-master). Thanks in any case!