-
- Downloads
tactic apply: add appropriate exception. simplify code and allow inductive
As a side effect, this also modifies reflection.ml accordingly. Conflicts: src/transform/reflection.ml
Showing
- examples/bts/126_apply.mlw 16 additions, 0 deletionsexamples/bts/126_apply.mlw
- examples/bts/126_apply/why3session.xml 41 additions, 0 deletionsexamples/bts/126_apply/why3session.xml
- examples/bts/126_apply/why3shapes.gz 0 additions, 0 deletionsexamples/bts/126_apply/why3shapes.gz
- src/session/itp_server.ml 2 additions, 0 deletionssrc/session/itp_server.ml
- src/transform/apply.ml 6 additions, 19 deletionssrc/transform/apply.ml
- src/transform/args_wrapper.ml 1 addition, 0 deletionssrc/transform/args_wrapper.ml
- src/transform/args_wrapper.mli 1 addition, 0 deletionssrc/transform/args_wrapper.mli
Loading
Please register or sign in to comment