Commit 3c56e1a6 authored by Heiko Becker's avatar Heiko Becker

Fix more bugs in certificate generation

parent ef7c0b45
......@@ -88,7 +88,7 @@ object CertificatePhase extends DaisyPhase {
textWithoutFCall + "\n\n" + functionCall
//append the output to the global string
fullCertificate = fullCertificate + "\n\n\n" + certificateText
fullCertificate = fullCertificate + "\n\n\n" + certificateText + "\n"
case None => reporter.fatalError ("No Precondition specified.")
}
......@@ -222,7 +222,7 @@ object CertificatePhase extends DaisyPhase {
}
private def coqUMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"Defintion UMin${nameOp} :exp Q := Unop Neg $nameOp", s"UMin${nameOp}.\n")
(s"Definition UMin${nameOp} :exp Q := Unop Neg $nameOp.\n", s"UMin${nameOp}")
private def hol4UMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"val UMin${nameOp} = Define `UMin${nameOp}:(real exp) = Unop Neg ${nameOp}`;\n",
......
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