Commit 9ad4f07f authored by Heiko Becker's avatar Heiko Becker

Fix bug in certificate generation for unary minus

parent 5007e897
......@@ -222,10 +222,10 @@ 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}")
(s"Defintion UMin${nameOp} :exp Q := Unop Neg $nameOp", s"UMin${nameOp}.\n")
private def hol4UMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"val UMin${nameOp} = Define `UMin${nameOp}:(real exp) = Unop Neg ${nameOp}`;",
(s"val UMin${nameOp} = Define `UMin${nameOp}:(real exp) = Unop Neg ${nameOp}`;\n",
s"UMin${nameOp}")
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = {
......
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