• Jacques-Henri Jourdan's avatar
    Make ProofMode tactics work in RO mode. · 8f523096
    Jacques-Henri Jourdan authored
    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.
    8f523096
ExampleListProofMode.v 13.7 KB