-
- Downloads
Merge branch 'feature/wp/cache-and-coq-context' into 'master'
Assure Why3 replays Coq proofs when the context changed See merge request frama-c/frama-c!2869
No related branches found
No related tags found
Showing
- src/plugins/wp/Cache.ml 10 additions, 0 deletionssrc/plugins/wp/Cache.ml
- src/plugins/wp/Cache.mli 1 addition, 0 deletionssrc/plugins/wp/Cache.mli
- src/plugins/wp/Changelog 1 addition, 1 deletionsrc/plugins/wp/Changelog
- src/plugins/wp/GuiGoal.ml 1 addition, 1 deletionsrc/plugins/wp/GuiGoal.ml
- src/plugins/wp/GuiNavigator.ml 12 additions, 12 deletionssrc/plugins/wp/GuiNavigator.ml
- src/plugins/wp/ProverCoq.ml 3 additions, 3 deletionssrc/plugins/wp/ProverCoq.ml
- src/plugins/wp/ProverErgo.ml 3 additions, 3 deletionssrc/plugins/wp/ProverErgo.ml
- src/plugins/wp/ProverScript.ml 1 addition, 1 deletionsrc/plugins/wp/ProverScript.ml
- src/plugins/wp/ProverWhy3.ml 58 additions, 24 deletionssrc/plugins/wp/ProverWhy3.ml
- src/plugins/wp/VCS.ml 16 additions, 10 deletionssrc/plugins/wp/VCS.ml
- src/plugins/wp/VCS.mli 10 additions, 8 deletionssrc/plugins/wp/VCS.mli
- src/plugins/wp/doc/manual/wp_plugin.tex 11 additions, 6 deletionssrc/plugins/wp/doc/manual/wp_plugin.tex
- src/plugins/wp/prover.ml 1 addition, 1 deletionsrc/plugins/wp/prover.ml
- src/plugins/wp/register.ml 2 additions, 2 deletionssrc/plugins/wp/register.ml
- src/plugins/wp/tests/wp/stmtcompiler_test.ml 1 addition, 1 deletionsrc/plugins/wp/tests/wp/stmtcompiler_test.ml
- src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml 1 addition, 1 deletionsrc/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
- src/plugins/wp/wp_parameters.ml 11 additions, 15 deletionssrc/plugins/wp/wp_parameters.ml
Loading
Please register or sign in to comment