GitLab

coq_makefile would have done this right...

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.