GitLab

Notations: use `` instead of ` for enc, in order to avoid compatibility with proj1_sig notation defined in Coq's Program.Util.

Generalization of xpull in the case of RO triples, which are not local.
ram_apply locks the intermediate assertion if the post-condition is an evar.
use rule_seq instead of rule_seq' in ExampleListProofMode.

Add a few proofmode type class instance for hpure and htop.

Cleanup SepLogic: move [hpure] in SepLogicSetup, define hand, hor hwand and hforall in SepLogicSetup, and avoid exporting SepLogicSetup when SepLogicTactics is already exported.

Change the ;; notation for Seq and use ;;;, so that it stays compatible with stdpp/iris. This is temporary, until we find a better solution.