This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.

I am now also using reification to obtain the indexes corresponding to
the stuff we want to cancel instead of relying on matching using Ltac.

With Set Printing All, these notations make me loose overview entirely.

barrier: strive for consistency between barrierGF and the inGF assumptions; also change some instance names

This reverts commit 7266d16b

And now the part that I forgot to commit.

I made the list of iFunctors monomorphic to avoid having to deal with
universe polymorphism, that is still somewhat flaky.

Also, give all these global functors the suffix GF to avoid shadowing
such as we had with authF.

And add some type annotations for clarity.

The non applied one should be only parsing.

due to an accidental git commit --amend after a git push.

In most cases there is a lot of duplicate proof search performed by
both naive_solver and eauto. Especially since naive_solver calls its
tactic (in the case of set_solver this used to be eauto) quite eagerly
this made it very slow.

Note that set_solver is this too slow and should be improved.

In most cases there is a lot of duplicate proof search performed by
both naive_solver and eauto. Especially since naive_solver calls its
tactic (in the case of set_solver this used to be eauto) quite eagerly
this made it very slow.

Note that set_solver is this too slow and should be improved.