• 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
Name
Last commit
Last update
attic Loading commit data...
dev Loading commit data...
doc Loading commit data...
examples Loading commit data...
generator Loading commit data...
lib Loading commit data...
model Loading commit data...
.gitignore Loading commit data...
INSTALL Loading commit data...
Makefile Loading commit data...
Makefile.common Loading commit data...
README.md Loading commit data...
TODO Loading commit data...
opam Loading commit data...
open.sh Loading commit data...