Skip to content
Snippets Groups Projects
Commit b3157364 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Change how postcond. are encoded in GroupedTactic

parent 0666b058
No related branches found
No related tags found
No related merge requests found
......@@ -20,7 +20,9 @@ class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
} yield {
implies(
precOrTrue(inComp),
application(p, Seq(b))
// @mk: Don't know which one is better. Inline the body, or have it as a fun. app?
//application(p, Seq(b))
application(p, Seq(FunctionInvocation(inComp.typedWithDef, inComp.params map { _.toVariable })))
)
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment