Remove a few mentions of mlnum

CakeML · Jan 19, 2019 · 48fec8b · 48fec8b
1 parent e8b6a02
commit 48fec8b
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 7 deletions.
diff --git a/basis/pure/basisComputeLib.sml b/basis/pure/basisComputeLib.sml
@@ -20,10 +20,7 @@ val add_basis_compset = computeLib.extend_compset
      mlintTheory.padLen_DEC_eq,
      mlintTheory.toChars_def,
      mlintTheory.toString_def,
-     mlnumTheory.toString_def,
-     mlnumTheory.num_toString_def,
-     mlnumTheory.fromString_def,
-     mlnumTheory.fromString_unsafe_def
+     mlintTheory.num_to_str_def
     ]
   ]
 

diff --git a/compiler/backend/proofs/word_elimProofScript.sml b/compiler/backend/proofs/word_elimProofScript.sml
@@ -2,7 +2,7 @@
   Correctness proof for word_elim
 *)
 
-open preamble backendComputeLib wordLangTheory
+open preamble wordLangTheory
      word_elimTheory wordSemTheory wordPropsTheory
      flat_elimProofTheory
 

diff --git a/examples/compilation/ag32/proofs/wordcountProofScript.sml b/examples/compilation/ag32/proofs/wordcountProofScript.sml
@@ -15,8 +15,8 @@ val is_ag32_init_state_def = ag32_targetTheory.is_ag32_init_state_def;
 
 (* TODO: move *)
 Theorem int_toString_num
-  `mlint$toString (&n) = mlnum$toString n`
-  (rw[mlintTheory.toString_thm, mlnumTheory.toString_thm]);
+  `mlint$toString ((&(n:num)):int) = toString n`
+  (rw[mlintTheory.num_to_str_def]);
 (* -- *)
 
 val wordcount_stdin_semantics = Q.prove(