Get Candle semantics to build again

CakeML · Jun 8, 2020 · 8366cf8 · 8366cf8
1 parent 3906239
commit 8366cf8
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/candle/standard/semantics/holAxiomsScript.sml b/candle/standard/semantics/holAxiomsScript.sml
@@ -6,6 +6,8 @@ open preamble holBoolTheory holBoolSyntaxTheory
      holSyntaxLibTheory holSyntaxTheory holSyntaxExtraTheory holAxiomsSyntaxTheory
      setSpecTheory holSemanticsTheory holSemanticsExtraTheory holExtensionTheory
 
+val _ = temp_delsimps ["NORMEQ_CONV"]
+
 val _ = new_theory"holAxioms"
 
 Overload A[local] = ``Tyvar (strlit "A")``

diff --git a/candle/standard/semantics/holBoolScript.sml b/candle/standard/semantics/holBoolScript.sml
@@ -5,6 +5,8 @@
 open preamble holSyntaxLibTheory holSyntaxTheory holSyntaxExtraTheory holBoolSyntaxTheory
      holSemanticsTheory holSemanticsExtraTheory setSpecTheory
 
+val _ = temp_delsimps ["NORMEQ_CONV"]
+
 val _ = new_theory"holBool"
 
 val _ = Parse.hide "mem";