GitLab

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.

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

This reverts commit 20b4ae55, which does
not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).

This makes type checking more directed, and somewhat more predictable.

On the downside, it makes it impossible to declare the singleton on
lists as an instance of SingletonM and the insert and alter operations
on functions as instances of Alter and Insert. However, these were not
used often anyway.

There was not really a need for the lattice type classes, so I removed
these.

This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.

This may save the need to seal off some stuff.

The singleton maps notation is now also more consistent with the
insert <[_ := _]> _ notation for maps.

Also, make our redefinition of done more robust under different
orders of Importing modules.

Since Coq 8.4 did not backtrack on eauto premises, we used to ensure
that hints like

  Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.

were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead
of _ ≡{_}≡ _.

This seems to be a legacy issue that no longer applies to Coq 8.5, so
I have removed these restrictions making these hints thus more powerful.

Also do some minor clean up.

These are hardly used, and confusing since we have so many operations of
different arities that distribute.