Commit f3e1a1f9 authored by Heiko Becker's avatar Heiko Becker

Fix linebreak bug in HOL certificates and include some beautifications in the...

Fix linebreak bug in HOL certificates and include some beautifications in the structure for readability
parent 0f33d0c0
......@@ -62,7 +62,7 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq")
textWithoutFCall + "\n\n" + functionCall
else
textWithoutFCall + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment