Try fixing some HOL4 eval issues

4884374c · Heiko Becker · c4af8f2b · 3f8f06e6 · 0f9a84cd · 3f8f06e6
Commit 4884374c authored Oct 03, 2017 by Heiko Becker
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 2 deletions

hol4/cakeml hol4/cakeml +1 -1

src/main/scala/daisy/backend/CertificatePhase.scala src/main/scala/daisy/backend/CertificatePhase.scala +1 -1

No files found.
--- a/cakeml @ 3f8f06e6
+++ b/cakeml @ 3f8f06e6
-Subproject commit 0f9a84cd5d6459117a10d5c60ced075cf312471b
+Subproject commit 3f8f06e6f46b79db0217c67bc1842309900666b4
--- a/src/main/scala/daisy/backend/CertificatePhase.scala
+++ b/src/main/scala/daisy/backend/CertificatePhase.scala
@@ -781,7 +781,7 @@ object CertificatePhase extends DaisyPhase {
      "Proof.\n  vm_compute; auto.\nQed.\n"
    } else if (prover == "hol4"){
      "val _ = store_thm (\""+s"ErrorBound_${fName}_Sound"+"\",\n" +
-      s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n EVAL_TAC);\n"
+      s"``CertificateCheckerCmd $lastGenName $analysisResultName $precondName $defVarsName``,\n EVAL_TAC \\ fs[]);\n"
    } else
      ""