Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
a5a4a2c5
Commit
a5a4a2c5
authored
Oct 16, 2020
by
Loïc Correnson
Committed by
Allan Blanchard
Oct 19, 2020
Browse files
[wp] commit all residuals in prover script
(cherry picked from commit c7db4956edbec05151fd4a298ae856a6ac10b404)
parent
b876bf4e
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/plugins/wp/ProverScript.ml
View file @
a5a4a2c5
...
...
@@ -322,9 +322,10 @@ let apply env node jtactic subscripts =
|
Some
fork
->
let
_
,
children
=
ProofEngine
.
commit
fork
in
reconcile
children
subscripts
;
(*TODO: saveback forgiven script ? *)
List
.
filter
(
fun
(
_
,
node
)
->
not
(
ProofEngine
.
proved
node
))
children
let
ok
=
List
.
for_all
(
fun
(
_
,
node
)
->
ProofEngine
.
proved
node
)
children
in
if
ok
then
[]
else
children
(* -------------------------------------------------------------------------- *)
(* --- Script Crawling --- *)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment